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/ftc/FunctSeries".
21 (* $Id: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
23 include "ftc/FunctSequence.ma".
25 include "reals/Series.ma".
27 (*#* printing fun_seq_part_sum %\ensuremath{\sum^n}% #∑<sup>n</sup># *)
29 (*#* printing Fun_Series_Sum %\ensuremath{\sum_0^{\infty}}% #∑<sub>0</sub><sup>∞</sup># *)
35 (*#* *Series of Functions
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.
41 %\begin{convention}% Throughout this section:
42 - [a] and [b] will be real numbers and the interval [[a,b]] will be denoted
44 - [f, g] and [h] will denote sequences of continuous functions;
45 - [F, G] and [H] will denote continuous functions.
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.
56 inline "cic:/CoRN/ftc/FunctSeries/a.var".
58 inline "cic:/CoRN/ftc/FunctSeries/b.var".
60 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
64 inline "cic:/CoRN/ftc/FunctSeries/I.con".
68 inline "cic:/CoRN/ftc/FunctSeries/f.var".
70 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum.con".
72 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_cont.con".
74 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent.con".
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
82 inline "cic:/CoRN/ftc/FunctSeries/fun_series_conv_imp_conv.con".
84 (*#* We then define the sum of the series as being the pointwise sum of
85 the corresponding series.
90 inline "cic:/CoRN/ftc/FunctSeries/H.var".
96 inline "cic:/CoRN/ftc/FunctSeries/contf.con".
98 inline "cic:/CoRN/ftc/FunctSeries/incf.con".
102 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_strext.con".
104 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum.con".
111 Implicit Arguments Fun_Series_Sum [a b Hab f].
115 Hint Resolve fun_seq_part_sum_cont: continuous.
119 Section More_Definitions.
122 inline "cic:/CoRN/ftc/FunctSeries/a.var".
124 inline "cic:/CoRN/ftc/FunctSeries/b.var".
126 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
128 inline "cic:/CoRN/ftc/FunctSeries/f.var".
130 (*#* A series can also be absolutely convergent. *)
132 inline "cic:/CoRN/ftc/FunctSeries/fun_series_abs_convergent.con".
135 End More_Definitions.
142 (* **Algebraic Properties
144 All of these are analogous to the properties for series of real numbers, so we won't comment much about them.
147 inline "cic:/CoRN/ftc/FunctSeries/a.var".
149 inline "cic:/CoRN/ftc/FunctSeries/b.var".
151 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
155 inline "cic:/CoRN/ftc/FunctSeries/I.con".
159 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_n.con".
161 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_const_series.con".
163 inline "cic:/CoRN/ftc/FunctSeries/fun_const_series_sum.con".
165 inline "cic:/CoRN/ftc/FunctSeries/conv_zero_fun_series.con".
167 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_zero.con".
171 inline "cic:/CoRN/ftc/FunctSeries/f.var".
173 inline "cic:/CoRN/ftc/FunctSeries/g.var".
177 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con".
181 inline "cic:/CoRN/ftc/FunctSeries/convF.var".
183 inline "cic:/CoRN/ftc/FunctSeries/convG.var".
187 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_wd'.con".
189 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_plus.con".
191 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_plus.con".
193 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_minus.con".
195 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_min.con".
198 %\begin{convention}% Let [c:IR].
202 inline "cic:/CoRN/ftc/FunctSeries/c.var".
204 inline "cic:/CoRN/ftc/FunctSeries/H.var".
206 inline "cic:/CoRN/ftc/FunctSeries/contH.var".
208 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_scal.con".
210 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_scal.con".
217 Section More_Operations.
220 inline "cic:/CoRN/ftc/FunctSeries/a.var".
222 inline "cic:/CoRN/ftc/FunctSeries/b.var".
224 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
228 inline "cic:/CoRN/ftc/FunctSeries/I.con".
232 inline "cic:/CoRN/ftc/FunctSeries/f.var".
234 inline "cic:/CoRN/ftc/FunctSeries/convF.var".
236 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_inv.con".
238 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_inv.con".
245 Section Other_Results.
248 inline "cic:/CoRN/ftc/FunctSeries/a.var".
250 inline "cic:/CoRN/ftc/FunctSeries/b.var".
252 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
254 inline "cic:/CoRN/ftc/FunctSeries/f.var".
256 inline "cic:/CoRN/ftc/FunctSeries/convF.var".
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
264 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char'.con".
266 inline "cic:/CoRN/ftc/FunctSeries/fun_series_conv.con".
268 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_cont.con".
270 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char.con".
272 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_as_Lim.con".
279 Hint Resolve Fun_Series_Sum_cont: continuous.
283 Section Convergence_Criteria.
286 (*#* **Convergence Criteria
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.
291 inline "cic:/CoRN/ftc/FunctSeries/a.var".
293 inline "cic:/CoRN/ftc/FunctSeries/b.var".
295 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
299 inline "cic:/CoRN/ftc/FunctSeries/I.con".
303 inline "cic:/CoRN/ftc/FunctSeries/f.var".
305 inline "cic:/CoRN/ftc/FunctSeries/contF.var".
324 Opaque fun_seq_part_sum.
340 Transparent fun_seq_part_sum.
344 Opaque fun_seq_part_sum.
347 inline "cic:/CoRN/ftc/FunctSeries/fun_str_comparison.con".
353 inline "cic:/CoRN/ftc/FunctSeries/fun_comparison.con".
355 inline "cic:/CoRN/ftc/FunctSeries/abs_imp_conv.con".
361 inline "cic:/CoRN/ftc/FunctSeries/fun_ratio_test_conv.con".
364 End Convergence_Criteria.