]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/FunctSums.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / FunctSums.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
18
19 include "CoRN.ma".
20
21 (* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
22
23 (*#* printing FSum0 %\ensuremath{\sum_0}% #&sum;<sub>0</sub># *)
24
25 (*#* printing FSum %\ensuremath{\sum}% #&sum;# *)
26
27 (*#* printing FSumx %\ensuremath{\sum'}% #&sum;'&*)
28
29 include "reals/CSumsReals.ma".
30
31 include "ftc/PartFunEquality.ma".
32
33 (*#* *Sums of Functions
34
35 In this file we define sums are defined of arbitrary families of
36 partial functions.
37
38 Given a countable family of functions, their sum is defined on the
39 intersection of all the domains.  As is the case for groups, we will
40 define three different kinds of sums.
41
42 We will first consider the case of a family
43 $\{f_i\}_{i\in\NN}$#{f<sub>i</sub>}# of functions; we can both define
44 $\sum_{i=0}^{n-1}f_i$#the sum of the first n functions# ( [FSum0]) or
45 $\sum_{i=m}^nf_i$#the sum of f<sub>m</sub> through f<sub>n</sub>#
46 ( [FSum]).
47 *)
48
49 inline "cic:/CoRN/ftc/FunctSums/FSum0.con".
50
51 inline "cic:/CoRN/ftc/FunctSums/FSum.con".
52
53 (*#*
54 Although [FSum] is here defined directly, it has the same relationship
55 to the [FSum0] operator as [Sum] has to [Sum0].  Also, all the results
56 for [Sum] and [Sum0] hold when these operators are replaced by their
57 functional equivalents.  This is an immediate consequence of the fact
58 that the partial functions form a group; however, as we already
59 mentioned, their forming too big a type makes it impossible to use
60 those results.
61 *)
62
63 inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0.con".
64
65 inline "cic:/CoRN/ftc/FunctSums/FSum0_wd.con".
66
67 inline "cic:/CoRN/ftc/FunctSums/FSum_one.con".
68
69 inline "cic:/CoRN/ftc/FunctSums/FSum_FSum.con".
70
71 inline "cic:/CoRN/ftc/FunctSums/FSum_first.con".
72
73 inline "cic:/CoRN/ftc/FunctSums/FSum_last.con".
74
75 inline "cic:/CoRN/ftc/FunctSums/FSum_last'.con".
76
77 inline "cic:/CoRN/ftc/FunctSums/FSum_wd.con".
78
79 inline "cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con".
80
81 inline "cic:/CoRN/ftc/FunctSums/inv_FSum.con".
82
83 inline "cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con".
84
85 inline "cic:/CoRN/ftc/FunctSums/FSum_wd'.con".
86
87 inline "cic:/CoRN/ftc/FunctSums/FSum_resp_less.con".
88
89 inline "cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con".
90
91 inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con".
92
93 inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con".
94
95 (*#*
96 Also important is the case when we have a finite family
97 $\{f_i\}_{i=0}^{n-1}$ of #exactly n# functions; in this case we need
98 to use the [FSumx] operator.
99 *)
100
101 inline "cic:/CoRN/ftc/FunctSums/FSumx.con".
102
103 (*#*
104 This operator is well defined, as expected.
105 *)
106
107 inline "cic:/CoRN/ftc/FunctSums/FSumx_wd.con".
108
109 inline "cic:/CoRN/ftc/FunctSums/FSumx_wd'.con".
110
111 (*#*
112 As was already the case for [Sumx], in many cases we will need to
113 explicitly assume that $f_i$#f<sub>1</sub># is independent of the proof that
114 [i [<] n].  This holds both for the value and the domain of the partial
115 function $f_i$#f<sub>i</sub>#.
116 *)
117
118 inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq.con".
119
120 inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con".
121
122 (* UNEXPORTED
123 Implicit Arguments ext_fun_seq [n].
124 *)
125
126 (* UNEXPORTED
127 Implicit Arguments ext_fun_seq' [n].
128 *)
129
130 (*#*
131 Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
132 *)
133
134 inline "cic:/CoRN/ftc/FunctSums/FSumx_pred.con".
135
136 inline "cic:/CoRN/ftc/FunctSums/FSumx_pred'.con".
137
138 inline "cic:/CoRN/ftc/FunctSums/FSumx_char.con".
139
140 (*#*
141 As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
142 *)
143
144 inline "cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con".
145
146 inline "cic:/CoRN/ftc/FunctSums/FSumx_lt.con".
147
148 inline "cic:/CoRN/ftc/FunctSums/FSumx_le.con".
149
150 inline "cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con".
151
152 (*#*
153 Some useful lemmas follow.
154 *)
155
156 inline "cic:/CoRN/ftc/FunctSums/FSum0_0.con".
157
158 inline "cic:/CoRN/ftc/FunctSums/FSum0_S.con".
159
160 inline "cic:/CoRN/ftc/FunctSums/FSum_0.con".
161
162 inline "cic:/CoRN/ftc/FunctSums/FSum_S.con".
163
164 inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con".
165