]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/FunctSeries.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / FunctSeries.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/FunctSeries".
18
19 include "CoRN.ma".
20
21 (* $Id: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
22
23 include "ftc/FunctSequence.ma".
24
25 include "reals/Series.ma".
26
27 (*#* printing fun_seq_part_sum %\ensuremath{\sum^n}% #&sum;<sup>n</sup># *)
28
29 (*#* printing Fun_Series_Sum %\ensuremath{\sum_0^{\infty}}% #&sum;<sub>0</sub><sup>&infin;</sup># *)
30
31 (* UNEXPORTED
32 Section Definitions
33 *)
34
35 (*#* *Series of Functions
36
37 We now turn our attention to series of functions.  Like it was already
38 the case for sequences, we will mainly rewrite the results we proved
39 for series of real numbers in a different way.
40
41 %\begin{convention}% Throughout this section:
42  - [a] and [b] will be real numbers and the interval [[a,b]] will be denoted
43 by [I];
44  - [f, g] and [h] will denote sequences of continuous functions;
45  - [F, G] and [H] will denote continuous functions.
46
47 %\end{convention}%
48
49 ** Definitions
50
51 As before, we will consider only sequences of continuous functions
52 defined in a compact interval.  For this, partial sums are defined and
53 convergence is simply the convergence of the sequence of partial sums.
54 *)
55
56 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Definitions/a.var".
57
58 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Definitions/b.var".
59
60 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Definitions/Hab.var".
61
62 (* begin hide *)
63
64 inline "cic:/CoRN/ftc/FunctSeries/Definitions/I.con" "Definitions__".
65
66 (* end hide *)
67
68 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Definitions/f.var".
69
70 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum.con".
71
72 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_cont.con".
73
74 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent.con".
75
76 (*#*
77 For what comes up next we need to know that the convergence of a
78 series of functions implies pointwise convergence of the corresponding
79 real number series.
80 *)
81
82 inline "cic:/CoRN/ftc/FunctSeries/fun_series_conv_imp_conv.con".
83
84 (*#* We then define the sum of the series as being the pointwise sum of
85 the corresponding series.
86 *)
87
88 (* begin show *)
89
90 alias id "H" = "cic:/CoRN/ftc/FunctSeries/Definitions/H.var".
91
92 (* end show *)
93
94 (* begin hide *)
95
96 inline "cic:/CoRN/ftc/FunctSeries/Definitions/contf.con" "Definitions__".
97
98 inline "cic:/CoRN/ftc/FunctSeries/Definitions/incf.con" "Definitions__".
99
100 (* end hide *)
101
102 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_strext.con".
103
104 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum.con".
105
106 (* UNEXPORTED
107 End Definitions
108 *)
109
110 (* UNEXPORTED
111 Implicit Arguments Fun_Series_Sum [a b Hab f].
112 *)
113
114 (* UNEXPORTED
115 Hint Resolve fun_seq_part_sum_cont: continuous.
116 *)
117
118 (* UNEXPORTED
119 Section More_Definitions
120 *)
121
122 alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/a.var".
123
124 alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/b.var".
125
126 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/Hab.var".
127
128 alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/f.var".
129
130 (*#* A series can also be absolutely convergent. *)
131
132 inline "cic:/CoRN/ftc/FunctSeries/fun_series_abs_convergent.con".
133
134 (* UNEXPORTED
135 End More_Definitions
136 *)
137
138 (* UNEXPORTED
139 Section Operations
140 *)
141
142 (* **Algebraic Properties
143
144 All of these are analogous to the properties for series of real numbers, so we won't comment much about them.
145 *)
146
147 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Operations/a.var".
148
149 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Operations/b.var".
150
151 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Operations/Hab.var".
152
153 (* begin hide *)
154
155 inline "cic:/CoRN/ftc/FunctSeries/Operations/I.con" "Operations__".
156
157 (* end hide *)
158
159 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_n.con".
160
161 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_const_series.con".
162
163 inline "cic:/CoRN/ftc/FunctSeries/fun_const_series_sum.con".
164
165 inline "cic:/CoRN/ftc/FunctSeries/conv_zero_fun_series.con".
166
167 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_zero.con".
168
169 (* begin show *)
170
171 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Operations/f.var".
172
173 alias id "g" = "cic:/CoRN/ftc/FunctSeries/Operations/g.var".
174
175 (* end show *)
176
177 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con".
178
179 (* begin show *)
180
181 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Operations/convF.var".
182
183 alias id "convG" = "cic:/CoRN/ftc/FunctSeries/Operations/convG.var".
184
185 (* end show *)
186
187 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_wd'.con".
188
189 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_plus.con".
190
191 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_plus.con".
192
193 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_minus.con".
194
195 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_min.con".
196
197 (*#*
198 %\begin{convention}% Let [c:IR].
199 %\end{convention}%
200 *)
201
202 alias id "c" = "cic:/CoRN/ftc/FunctSeries/Operations/c.var".
203
204 alias id "H" = "cic:/CoRN/ftc/FunctSeries/Operations/H.var".
205
206 alias id "contH" = "cic:/CoRN/ftc/FunctSeries/Operations/contH.var".
207
208 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_scal.con".
209
210 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_scal.con".
211
212 (* UNEXPORTED
213 End Operations
214 *)
215
216 (* UNEXPORTED
217 Section More_Operations
218 *)
219
220 alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Operations/a.var".
221
222 alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Operations/b.var".
223
224 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Operations/Hab.var".
225
226 (* begin hide *)
227
228 inline "cic:/CoRN/ftc/FunctSeries/More_Operations/I.con" "More_Operations__".
229
230 (* end hide *)
231
232 alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Operations/f.var".
233
234 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/More_Operations/convF.var".
235
236 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_inv.con".
237
238 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_inv.con".
239
240 (* UNEXPORTED
241 End More_Operations
242 *)
243
244 (* UNEXPORTED
245 Section Other_Results
246 *)
247
248 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Other_Results/a.var".
249
250 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Other_Results/b.var".
251
252 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Other_Results/Hab.var".
253
254 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Other_Results/f.var".
255
256 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Other_Results/convF.var".
257
258 (*#*
259 The following relate the sum series with the limit of the sequence of
260 partial sums; as a corollary we get the continuity of the sum of the
261 series.
262 *)
263
264 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char'.con".
265
266 inline "cic:/CoRN/ftc/FunctSeries/fun_series_conv.con".
267
268 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_cont.con".
269
270 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char.con".
271
272 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_as_Lim.con".
273
274 (* UNEXPORTED
275 End Other_Results
276 *)
277
278 (* UNEXPORTED
279 Hint Resolve Fun_Series_Sum_cont: continuous.
280 *)
281
282 (* UNEXPORTED
283 Section Convergence_Criteria
284 *)
285
286 (*#* **Convergence Criteria
287
288 Most of the convergence criteria for series of real numbers carry over to series of real-valued functions, so again we just present them without comments.
289 *)
290
291 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/a.var".
292
293 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/b.var".
294
295 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/Hab.var".
296
297 (* begin hide *)
298
299 inline "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/I.con" "Convergence_Criteria__".
300
301 (* end hide *)
302
303 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/f.var".
304
305 alias id "contF" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/contF.var".
306
307 (* UNEXPORTED
308 Opaque Frestr.
309 *)
310
311 (* UNEXPORTED
312 Transparent Frestr.
313 *)
314
315 (* UNEXPORTED
316 Opaque FAbs.
317 *)
318
319 (* UNEXPORTED
320 Transparent FAbs.
321 *)
322
323 (* UNEXPORTED
324 Opaque fun_seq_part_sum.
325 *)
326
327 (* UNEXPORTED
328 Opaque FAbs.
329 *)
330
331 (* UNEXPORTED
332 Transparent FAbs.
333 *)
334
335 (* UNEXPORTED
336 Opaque FAbs.
337 *)
338
339 (* UNEXPORTED
340 Transparent fun_seq_part_sum.
341 *)
342
343 (* UNEXPORTED
344 Opaque fun_seq_part_sum.
345 *)
346
347 inline "cic:/CoRN/ftc/FunctSeries/fun_str_comparison.con".
348
349 (* UNEXPORTED
350 Transparent FAbs.
351 *)
352
353 inline "cic:/CoRN/ftc/FunctSeries/fun_comparison.con".
354
355 inline "cic:/CoRN/ftc/FunctSeries/abs_imp_conv.con".
356
357 (* UNEXPORTED
358 Opaque FAbs.
359 *)
360
361 inline "cic:/CoRN/ftc/FunctSeries/fun_ratio_test_conv.con".
362
363 (* UNEXPORTED
364 End Convergence_Criteria
365 *)
366