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: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
21 include "ftc/FunctSequence.ma".
23 include "reals/Series.ma".
25 (*#* printing fun_seq_part_sum %\ensuremath{\sum^n}% #∑<sup>n</sup># *)
27 (*#* printing Fun_Series_Sum %\ensuremath{\sum_0^{\infty}}% #∑<sub>0</sub><sup>∞</sup># *)
33 (*#* *Series of Functions
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.
39 %\begin{convention}% Throughout this section:
40 - [a] and [b] will be real numbers and the interval [[a,b]] will be denoted
42 - [f, g] and [h] will denote sequences of continuous functions;
43 - [F, G] and [H] will denote continuous functions.
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.
54 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Definitions/a.var".
56 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Definitions/b.var".
58 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Definitions/Hab.var".
62 inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/I.con" "Definitions__".
66 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Definitions/f.var".
68 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum.con".
70 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_cont.con".
72 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_convergent.con".
75 For what comes up next we need to know that the convergence of a
76 series of functions implies pointwise convergence of the corresponding
80 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_conv_imp_conv.con".
82 (*#* We then define the sum of the series as being the pointwise sum of
83 the corresponding series.
88 alias id "H" = "cic:/CoRN/ftc/FunctSeries/Definitions/H.var".
94 inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/contf.con" "Definitions__".
96 inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/incf.con" "Definitions__".
100 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_strext.con".
102 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum.con".
109 Implicit Arguments Fun_Series_Sum [a b Hab f].
113 Hint Resolve fun_seq_part_sum_cont: continuous.
117 Section More_Definitions
120 alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/a.var".
122 alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/b.var".
124 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/Hab.var".
126 alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/f.var".
128 (*#* A series can also be absolutely convergent. *)
130 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_abs_convergent.con".
140 (* **Algebraic Properties
142 All of these are analogous to the properties for series of real numbers, so we won't comment much about them.
145 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Operations/a.var".
147 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Operations/b.var".
149 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Operations/Hab.var".
153 inline procedural "cic:/CoRN/ftc/FunctSeries/Operations/I.con" "Operations__".
157 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_n.con".
159 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_const_series.con".
161 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_const_series_sum.con".
163 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_zero_fun_series.con".
165 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_zero.con".
169 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Operations/f.var".
171 alias id "g" = "cic:/CoRN/ftc/FunctSeries/Operations/g.var".
175 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con".
179 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Operations/convF.var".
181 alias id "convG" = "cic:/CoRN/ftc/FunctSeries/Operations/convG.var".
185 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_wd'.con".
187 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_plus.con".
189 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_plus.con".
191 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_minus.con".
193 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_min.con".
196 %\begin{convention}% Let [c:IR].
200 alias id "c" = "cic:/CoRN/ftc/FunctSeries/Operations/c.var".
202 alias id "H" = "cic:/CoRN/ftc/FunctSeries/Operations/H.var".
204 alias id "contH" = "cic:/CoRN/ftc/FunctSeries/Operations/contH.var".
206 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_scal.con".
208 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_scal.con".
215 Section More_Operations
218 alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Operations/a.var".
220 alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Operations/b.var".
222 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Operations/Hab.var".
226 inline procedural "cic:/CoRN/ftc/FunctSeries/More_Operations/I.con" "More_Operations__".
230 alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Operations/f.var".
232 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/More_Operations/convF.var".
234 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_inv.con".
236 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_inv.con".
243 Section Other_Results
246 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Other_Results/a.var".
248 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Other_Results/b.var".
250 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Other_Results/Hab.var".
252 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Other_Results/f.var".
254 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Other_Results/convF.var".
257 The following relate the sum series with the limit of the sequence of
258 partial sums; as a corollary we get the continuity of the sum of the
262 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char'.con".
264 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_conv.con".
266 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_cont.con".
268 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char.con".
270 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_as_Lim.con".
277 Hint Resolve Fun_Series_Sum_cont: continuous.
281 Section Convergence_Criteria
284 (*#* **Convergence Criteria
286 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 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/a.var".
291 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/b.var".
293 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/Hab.var".
297 inline procedural "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/I.con" "Convergence_Criteria__".
301 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/f.var".
303 alias id "contF" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/contF.var".
322 Opaque fun_seq_part_sum.
338 Transparent fun_seq_part_sum.
342 Opaque fun_seq_part_sum.
345 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_str_comparison.con".
351 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_comparison.con".
353 inline procedural "cic:/CoRN/ftc/FunctSeries/abs_imp_conv.con".
359 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_ratio_test_conv.con".
362 End Convergence_Criteria