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