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: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
21 include "ftc/FunctSeries.ma".
23 include "ftc/MoreFunctions.ma".
25 (*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #∑'<sub>∞</sub># *)
31 (*#* *More on Sequences and Series
33 We will now extend our convergence definitions and results for
34 sequences and series of functions defined in compact intervals to
37 %\begin{convention}% Throughout this file, [J] will be an interval,
38 [f, g] will be sequences of continuous (in [J]) functions and [F,G]
39 will be continuous (in [J]) functions.
44 First we will consider the case of sequences.
48 Some of the definitions do not make sense in this more general setting
49 (for instance, because the norm of a function is no longer defined),
50 but the ones which do we simply adapt in the usual way.
53 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/J.var".
55 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/f.var".
57 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/F.var".
59 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contf.var".
61 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contF.var".
63 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con".
65 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con".
67 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con".
69 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con".
72 The equivalences between these definitions still hold.
75 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con".
77 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con".
79 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con".
81 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con".
88 Section More_Definitions
92 Limit is defined and works in the same way as before.
95 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/J.var".
97 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/f.var".
99 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/contf.var".
103 alias id "conv" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/conv.var".
107 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con".
109 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con".
116 Section Irrelevance_of_Proofs
119 (*#* ***Basic Properties
121 Proofs are irrelevant as before---they just have to be present.
124 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/J.var".
126 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/f.var".
130 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf.var".
132 alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf0.var".
136 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/F.var".
140 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF.var".
142 alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF0.var".
146 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con".
148 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con".
150 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con".
153 End Irrelevance_of_Proofs
157 Opaque Cauchy_fun_seq_Lim_IR.
161 Section More_Properties
164 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/J.var".
166 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/f.var".
168 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/g.var".
172 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf.var".
174 alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf0.var".
176 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg.var".
178 alias id "contg0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg0.var".
182 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con".
184 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/F.var".
186 alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/G.var".
190 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF.var".
192 alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF0.var".
194 alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG.var".
196 alias id "contG0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG0.var".
200 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con".
202 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con".
204 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con".
206 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con".
208 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con".
210 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con".
212 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con".
219 Hint Resolve Cauchy_cont_Lim_IR: continuous.
223 Section Algebraic_Properties
226 (*#* ***Algebraic Properties
228 Algebraic operations still work well.
231 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/J.var".
233 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/f.var".
235 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/g.var".
237 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contf.var".
239 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contg.var".
241 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con".
243 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con".
245 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con".
247 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con".
249 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/F.var".
251 alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/G.var".
253 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contF.var".
255 alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contG.var".
259 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convF.var".
261 alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convG.var".
265 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con".
267 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con".
269 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con".
272 End Algebraic_Properties
276 Section More_Algebraic_Properties
280 If we work with the limit function things fit in just as well.
283 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/J.var".
285 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/f.var".
287 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/g.var".
289 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contf.var".
291 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contg.var".
295 alias id "Hf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hf.var".
297 alias id "Hg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hg.var".
301 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con".
303 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con".
305 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con".
307 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con".
309 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con".
311 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con".
313 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con".
315 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con".
318 End More_Algebraic_Properties
325 (*#* ***Miscellaneous
327 Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
330 inline procedural "cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con".
332 inline procedural "cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con".
335 Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
338 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con".
345 Section Series_Definitions
350 We now consider series of functions defined in arbitrary intervals.
352 Convergence is defined as expected---through convergence in every compact interval.
355 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/J.var".
357 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/f.var".
359 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con".
361 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con".
365 alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/H.var".
369 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con".
371 (*#* Assume [h(x)] is the pointwise series of [f(x)] *)
375 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/h.con" "Series_Definitions__".
379 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con".
381 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con".
383 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con".
386 End Series_Definitions
390 Implicit Arguments FSeries_Sum [J f].
394 Section More_Series_Definitions
397 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/J.var".
399 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/f.var".
402 Absolute convergence still exists.
405 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con".
408 End More_Series_Definitions
412 Section Convergence_Results
416 As before, any series converges to its sum.
419 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/J.var".
421 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/f.var".
423 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con".
425 inline procedural "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con".
427 inline procedural "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con".
429 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con".
432 End Convergence_Results
436 Hint Resolve convergent_imp_inc: included.
440 Hint Resolve convergent_imp_Continuous Continuous_FSeries_Sum: continuous.
447 (*#* **Algebraic Operations
449 Convergence is well defined and preserved by operations.
452 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Operations/J.var".
454 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con".
456 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con".
458 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con".
460 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con".
462 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Operations/f.var".
464 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Operations/g.var".
466 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con".
470 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convF.var".
472 alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convG.var".
476 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con".
478 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con".
480 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con".
482 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con".
484 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con".
486 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con".
488 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con".
491 %\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
495 alias id "c" = "cic:/CoRN/ftc/MoreFunSeries/Operations/c.var".
497 alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Operations/H.var".
499 alias id "contH" = "cic:/CoRN/ftc/MoreFunSeries/Operations/contH.var".
501 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con".
503 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con".
510 Section Convergence_Criteria
513 (*#* ***Convergence Criteria
515 The most important tests for convergence of series still apply: the
516 comparison test (in both versions) and the ratio test.
519 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/J.var".
521 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/f.var".
523 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/contF.var".
525 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con".
527 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con".
529 inline procedural "cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con".
531 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con".
534 End Convergence_Criteria
538 Section Insert_Series
543 When working in particular with power series and Taylor series, it is
544 sometimes useful to ``shift'' all the terms in the series one position
545 forward, that is, replacing each $f_{i+1}$#f<sub>i+1</sub># with
546 $f_i$#f<sub>i</sub># and inserting the null function in the first
547 position. This does not affect convergence or the sum of the series.
550 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/J.var".
552 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/f.var".
554 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/convF.var".
556 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series.con".
558 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con".
560 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con".
562 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con".
564 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con".