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/MoreFunSeries".
21 (* $Id: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
23 include "ftc/FunctSeries.ma".
25 include "ftc/MoreFunctions.ma".
27 (*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #∑'<sub>∞</sub># *)
33 (*#* *More on Sequences and Series
35 We will now extend our convergence definitions and results for
36 sequences and series of functions defined in compact intervals to
39 %\begin{convention}% Throughout this file, [J] will be an interval,
40 [f, g] will be sequences of continuous (in [J]) functions and [F,G]
41 will be continuous (in [J]) functions.
46 First we will consider the case of sequences.
50 Some of the definitions do not make sense in this more general setting
51 (for instance, because the norm of a function is no longer defined),
52 but the ones which do we simply adapt in the usual way.
55 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
57 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
59 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
61 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
63 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
65 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con".
67 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con".
69 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con".
71 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con".
74 The equivalences between these definitions still hold.
77 inline "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con".
79 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con".
81 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con".
83 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con".
90 Section More_Definitions.
94 Limit is defined and works in the same way as before.
97 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
99 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
101 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
105 inline "cic:/CoRN/ftc/MoreFunSeries/conv.var".
109 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con".
111 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con".
114 End More_Definitions.
118 Section Irrelevance_of_Proofs.
121 (*#* ***Basic Properties
123 Proofs are irrelevant as before---they just have to be present.
126 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
128 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
132 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
134 inline "cic:/CoRN/ftc/MoreFunSeries/contf0.var".
138 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
142 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
144 inline "cic:/CoRN/ftc/MoreFunSeries/contF0.var".
148 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con".
150 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con".
152 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con".
155 End Irrelevance_of_Proofs.
159 Opaque Cauchy_fun_seq_Lim_IR.
163 Section More_Properties.
166 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
168 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
170 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
174 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
176 inline "cic:/CoRN/ftc/MoreFunSeries/contf0.var".
178 inline "cic:/CoRN/ftc/MoreFunSeries/contg.var".
180 inline "cic:/CoRN/ftc/MoreFunSeries/contg0.var".
184 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con".
186 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
188 inline "cic:/CoRN/ftc/MoreFunSeries/G.var".
192 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
194 inline "cic:/CoRN/ftc/MoreFunSeries/contF0.var".
196 inline "cic:/CoRN/ftc/MoreFunSeries/contG.var".
198 inline "cic:/CoRN/ftc/MoreFunSeries/contG0.var".
202 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con".
204 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con".
206 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con".
208 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con".
210 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con".
212 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con".
214 inline "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con".
221 Hint Resolve Cauchy_cont_Lim_IR: continuous.
225 Section Algebraic_Properties.
228 (*#* ***Algebraic Properties
230 Algebraic operations still work well.
233 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
235 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
237 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
239 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
241 inline "cic:/CoRN/ftc/MoreFunSeries/contg.var".
243 inline "cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con".
245 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con".
247 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con".
249 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con".
251 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
253 inline "cic:/CoRN/ftc/MoreFunSeries/G.var".
255 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
257 inline "cic:/CoRN/ftc/MoreFunSeries/contG.var".
261 inline "cic:/CoRN/ftc/MoreFunSeries/convF.var".
263 inline "cic:/CoRN/ftc/MoreFunSeries/convG.var".
267 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con".
269 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con".
271 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con".
274 End Algebraic_Properties.
278 Section More_Algebraic_Properties.
282 If we work with the limit function things fit in just as well.
285 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
287 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
289 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
291 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
293 inline "cic:/CoRN/ftc/MoreFunSeries/contg.var".
297 inline "cic:/CoRN/ftc/MoreFunSeries/Hf.var".
299 inline "cic:/CoRN/ftc/MoreFunSeries/Hg.var".
303 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con".
305 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con".
307 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con".
309 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con".
311 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con".
313 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con".
315 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con".
317 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con".
320 End More_Algebraic_Properties.
327 (*#* ***Miscellaneous
329 Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
332 inline "cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con".
334 inline "cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con".
337 Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
340 inline "cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con".
347 Section Series_Definitions.
352 We now consider series of functions defined in arbitrary intervals.
354 Convergence is defined as expected---through convergence in every compact interval.
357 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
359 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
361 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con".
363 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con".
367 inline "cic:/CoRN/ftc/MoreFunSeries/H.var".
371 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con".
373 (*#* Assume [h(x)] is the pointwise series of [f(x)] *)
377 inline "cic:/CoRN/ftc/MoreFunSeries/h.con".
381 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con".
383 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con".
385 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con".
388 End Series_Definitions.
392 Implicit Arguments FSeries_Sum [J f].
396 Section More_Series_Definitions.
399 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
401 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
404 Absolute convergence still exists.
407 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con".
410 End More_Series_Definitions.
414 Section Convergence_Results.
418 As before, any series converges to its sum.
421 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
423 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
425 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con".
427 inline "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con".
429 inline "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con".
431 inline "cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con".
434 End Convergence_Results.
438 Hint Resolve convergent_imp_inc: included.
442 Hint Resolve convergent_imp_Continuous Continuous_FSeries_Sum: continuous.
449 (*#* **Algebraic Operations
451 Convergence is well defined and preserved by operations.
454 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
456 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con".
458 inline "cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con".
460 inline "cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con".
462 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con".
464 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
466 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
468 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con".
472 inline "cic:/CoRN/ftc/MoreFunSeries/convF.var".
474 inline "cic:/CoRN/ftc/MoreFunSeries/convG.var".
478 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con".
480 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con".
482 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con".
484 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con".
486 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con".
488 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con".
490 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con".
493 %\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
497 inline "cic:/CoRN/ftc/MoreFunSeries/c.var".
499 inline "cic:/CoRN/ftc/MoreFunSeries/H.var".
501 inline "cic:/CoRN/ftc/MoreFunSeries/contH.var".
503 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con".
505 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con".
512 Section Convergence_Criteria.
515 (*#* ***Convergence Criteria
517 The most important tests for convergence of series still apply: the
518 comparison test (in both versions) and the ratio test.
521 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
523 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
525 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
527 inline "cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con".
529 inline "cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con".
531 inline "cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con".
533 inline "cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con".
536 End Convergence_Criteria.
540 Section Insert_Series.
545 When working in particular with power series and Taylor series, it is
546 sometimes useful to ``shift'' all the terms in the series one position
547 forward, that is, replacing each $f_{i+1}$#f<sub>i+1</sub># with
548 $f_i$#f<sub>i</sub># and inserting the null function in the first
549 position. This does not affect convergence or the sum of the series.
552 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
554 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
556 inline "cic:/CoRN/ftc/MoreFunSeries/convF.var".
558 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series.con".
560 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con".
562 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con".
564 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con".
566 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con".