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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
19 (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
21 (*#* printing Sum0 %\ensuremath{\sum_0}% #∑<sub>0</sub># *)
23 (*#* printing Sum1 %\ensuremath{\sum_1}% #∑<sub>1</sub># *)
25 (*#* printing Sum2 %\ensuremath{\sum_2}% #∑<sub>2</sub># *)
27 (*#* printing Sum %\ensuremath{\sum}% #∑# *)
29 (*#* printing Sumx %\ensuremath{\sum'}% #∑'&*)
41 %\begin{convention}% Let [G] be an abelian group.
49 inline cic:/CoRN/algebra/CSums/G.var.
51 (* Sum1 and Sum use subtraction *)
53 inline cic:/CoRN/algebra/CSums/Sumlist.con.
55 inline cic:/CoRN/algebra/CSums/Sumx.con.
58 It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$
59 #{0, ... i-1}# as a function on the natural numbers which evaluates to
60 [Zero] when the input is greater than or equal to [i].
63 inline cic:/CoRN/algebra/CSums/part_tot_nat_fun.con.
65 inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con.
67 inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con.
69 (*#* [Sum0] defines the sum for [i=0..(n-1)] *)
71 inline cic:/CoRN/algebra/CSums/Sum0.con.
73 (*#* [Sum1] defines the sum for [i=m..(n-1)] *)
75 inline cic:/CoRN/algebra/CSums/Sum1.con.
77 inline cic:/CoRN/algebra/CSums/Sum.con.
81 (*#* [Sum2] is similar to [Sum1], but does not require the summand to be
82 defined outside where it is being added. *)
84 inline cic:/CoRN/algebra/CSums/Sum2.con.
86 inline cic:/CoRN/algebra/CSums/Sum_one.con.
89 Hint Resolve Sum_one: algebra.
92 inline cic:/CoRN/algebra/CSums/Sum_empty.con.
95 Hint Resolve Sum_empty: algebra.
98 inline cic:/CoRN/algebra/CSums/Sum_Sum.con.
101 Hint Resolve Sum_Sum: algebra.
104 inline cic:/CoRN/algebra/CSums/Sum_first.con.
106 inline cic:/CoRN/algebra/CSums/Sum_last.con.
109 Hint Resolve Sum_last: algebra.
112 inline cic:/CoRN/algebra/CSums/Sum_last'.con.
115 We add some extensionality results which will be quite useful
116 when working with integration.
119 inline cic:/CoRN/algebra/CSums/Sum0_strext.con.
121 inline cic:/CoRN/algebra/CSums/Sum_strext.con.
123 inline cic:/CoRN/algebra/CSums/Sumx_strext.con.
125 inline cic:/CoRN/algebra/CSums/Sum0_strext'.con.
127 inline cic:/CoRN/algebra/CSums/Sum_strext'.con.
129 inline cic:/CoRN/algebra/CSums/Sum0_wd.con.
131 inline cic:/CoRN/algebra/CSums/Sum_wd.con.
133 inline cic:/CoRN/algebra/CSums/Sumx_wd.con.
135 inline cic:/CoRN/algebra/CSums/Sum_wd'.con.
137 inline cic:/CoRN/algebra/CSums/Sum2_wd.con.
139 inline cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con.
142 Hint Resolve Sum0_plus_Sum0: algebra.
145 inline cic:/CoRN/algebra/CSums/Sum_plus_Sum.con.
147 inline cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con.
149 inline cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con.
151 inline cic:/CoRN/algebra/CSums/inv_Sum0.con.
154 Hint Resolve inv_Sum0: algebra.
157 inline cic:/CoRN/algebra/CSums/inv_Sum.con.
160 Hint Resolve inv_Sum: algebra.
163 inline cic:/CoRN/algebra/CSums/inv_Sumx.con.
165 inline cic:/CoRN/algebra/CSums/inv_Sum2.con.
167 inline cic:/CoRN/algebra/CSums/Sum_minus_Sum.con.
170 Hint Resolve Sum_minus_Sum: algebra.
173 inline cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con.
175 inline cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con.
177 inline cic:/CoRN/algebra/CSums/Sum_apzero.con.
179 inline cic:/CoRN/algebra/CSums/Sum_zero.con.
181 inline cic:/CoRN/algebra/CSums/Sum_term.con.
183 inline cic:/CoRN/algebra/CSums/Sum0_shift.con.
186 Hint Resolve Sum0_shift: algebra.
189 inline cic:/CoRN/algebra/CSums/Sum_shift.con.
191 inline cic:/CoRN/algebra/CSums/Sum_big_shift.con.
193 inline cic:/CoRN/algebra/CSums/Sumx_Sum0.con.
200 Implicit Arguments Sum [G].
204 Implicit Arguments Sum0 [G].
208 Implicit Arguments Sumx [G n].
212 Implicit Arguments Sum2 [G m n].
216 The next results are useful for calculating some special sums,
217 often referred to as ``Mengolli Sums''.
218 %\begin{convention}% Let [G] be an abelian group.
226 inline cic:/CoRN/algebra/CSums/G.var.
228 inline cic:/CoRN/algebra/CSums/Mengolli_Sum.con.
230 inline cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con.
232 inline cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con.
234 inline cic:/CoRN/algebra/CSums/Sumx_to_Sum.con.
241 Hint Resolve Sum_one Sum_Sum Sum_first Sum_last Sum_last' Sum_wd
242 Sum_plus_Sum: algebra.
246 Hint Resolve Sum_minus_Sum inv_Sum inv_Sum0: algebra.