1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
21 (*#* printing FSum0 %\ensuremath{\sum_0}% #∑<sub>0</sub># *)
23 (*#* printing FSum %\ensuremath{\sum}% #∑# *)
25 (*#* printing FSumx %\ensuremath{\sum'}% #∑'&*)
27 include "reals/CSumsReals.ma".
29 include "ftc/PartFunEquality.ma".
31 (*#* *Sums of Functions
33 In this file we define sums are defined of arbitrary families of
36 Given a countable family of functions, their sum is defined on the
37 intersection of all the domains. As is the case for groups, we will
38 define three different kinds of sums.
40 We will first consider the case of a family
41 $\{f_i\}_{i\in\NN}$#{f<sub>i</sub>}# of functions; we can both define
42 $\sum_{i=0}^{n-1}f_i$#the sum of the first n functions# ( [FSum0]) or
43 $\sum_{i=m}^nf_i$#the sum of f<sub>m</sub> through f<sub>n</sub>#
47 inline procedural "cic:/CoRN/ftc/FunctSums/FSum0.con" as definition.
49 inline procedural "cic:/CoRN/ftc/FunctSums/FSum.con" as definition.
52 Although [FSum] is here defined directly, it has the same relationship
53 to the [FSum0] operator as [Sum] has to [Sum0]. Also, all the results
54 for [Sum] and [Sum0] hold when these operators are replaced by their
55 functional equivalents. This is an immediate consequence of the fact
56 that the partial functions form a group; however, as we already
57 mentioned, their forming too big a type makes it impossible to use
61 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_FSum0.con" as lemma.
63 inline procedural "cic:/CoRN/ftc/FunctSums/FSum0_wd.con" as lemma.
65 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_one.con" as lemma.
67 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_FSum.con" as lemma.
69 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_first.con" as lemma.
71 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_last.con" as lemma.
73 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_last'.con" as lemma.
75 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_wd.con" as lemma.
77 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con" as lemma.
79 inline procedural "cic:/CoRN/ftc/FunctSums/inv_FSum.con" as lemma.
81 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con" as lemma.
83 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_wd'.con" as lemma.
85 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_resp_less.con" as lemma.
87 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con" as lemma.
89 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con" as lemma.
91 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con" as lemma.
94 Also important is the case when we have a finite family
95 $\{f_i\}_{i=0}^{n-1}$ of #exactly n# functions; in this case we need
96 to use the [FSumx] operator.
99 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx.con" as definition.
102 This operator is well defined, as expected.
105 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_wd.con" as lemma.
107 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_wd'.con" as lemma.
110 As was already the case for [Sumx], in many cases we will need to
111 explicitly assume that $f_i$#f<sub>1</sub># is independent of the proof that
112 [i [<] n]. This holds both for the value and the domain of the partial
113 function $f_i$#f<sub>i</sub>#.
116 inline procedural "cic:/CoRN/ftc/FunctSums/ext_fun_seq.con" as definition.
118 inline procedural "cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con" as definition.
121 Implicit Arguments ext_fun_seq [n].
125 Implicit Arguments ext_fun_seq' [n].
129 Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
132 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_pred.con" as lemma.
134 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_pred'.con" as lemma.
136 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_char.con" as lemma.
139 As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
142 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con" as definition.
144 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_lt.con" as lemma.
146 inline procedural "cic:/CoRN/ftc/FunctSums/FSumx_le.con" as lemma.
148 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con" as lemma.
151 Some useful lemmas follow.
154 inline procedural "cic:/CoRN/ftc/FunctSums/FSum0_0.con" as lemma.
156 inline procedural "cic:/CoRN/ftc/FunctSums/FSum0_S.con" as lemma.
158 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_0.con" as lemma.
160 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_S.con" as lemma.
162 inline procedural "cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con" as lemma.