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".
19 (* $Id: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
29 (*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #∑'<sub>∞</sub># *)
35 (*#* *More on Sequences and Series
37 We will now extend our convergence definitions and results for
38 sequences and series of functions defined in compact intervals to
41 %\begin{convention}% Throughout this file, [J] will be an interval,
42 [f, g] will be sequences of continuous (in [J]) functions and [F,G]
43 will be continuous (in [J]) functions.
48 First we will consider the case of sequences.
52 Some of the definitions do not make sense in this more general setting
53 (for instance, because the norm of a function is no longer defined),
54 but the ones which do we simply adapt in the usual way.
57 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
59 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
61 inline cic:/CoRN/ftc/MoreFunSeries/F.var.
63 inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
65 inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
67 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con.
69 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con.
71 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con.
73 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con.
76 The equivalences between these definitions still hold.
79 inline cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con.
81 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con.
83 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con.
85 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con.
92 Section More_Definitions.
96 Limit is defined and works in the same way as before.
99 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
101 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
103 inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
107 inline cic:/CoRN/ftc/MoreFunSeries/conv.var.
111 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con.
113 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con.
116 End More_Definitions.
120 Section Irrelevance_of_Proofs.
123 (*#* ***Basic Properties
125 Proofs are irrelevant as before---they just have to be present.
128 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
130 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
134 inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
136 inline cic:/CoRN/ftc/MoreFunSeries/contf0.var.
140 inline cic:/CoRN/ftc/MoreFunSeries/F.var.
144 inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
146 inline cic:/CoRN/ftc/MoreFunSeries/contF0.var.
150 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con.
152 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con.
154 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con.
157 End Irrelevance_of_Proofs.
161 Opaque Cauchy_fun_seq_Lim_IR.
165 Section More_Properties.
168 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
170 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
172 inline cic:/CoRN/ftc/MoreFunSeries/g.var.
176 inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
178 inline cic:/CoRN/ftc/MoreFunSeries/contf0.var.
180 inline cic:/CoRN/ftc/MoreFunSeries/contg.var.
182 inline cic:/CoRN/ftc/MoreFunSeries/contg0.var.
186 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con.
188 inline cic:/CoRN/ftc/MoreFunSeries/F.var.
190 inline cic:/CoRN/ftc/MoreFunSeries/G.var.
194 inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
196 inline cic:/CoRN/ftc/MoreFunSeries/contF0.var.
198 inline cic:/CoRN/ftc/MoreFunSeries/contG.var.
200 inline cic:/CoRN/ftc/MoreFunSeries/contG0.var.
204 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con.
206 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con.
208 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con.
210 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con.
212 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con.
214 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con.
216 inline cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con.
223 Hint Resolve Cauchy_cont_Lim_IR: continuous.
227 Section Algebraic_Properties.
230 (*#* ***Algebraic Properties
232 Algebraic operations still work well.
235 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
237 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
239 inline cic:/CoRN/ftc/MoreFunSeries/g.var.
241 inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
243 inline cic:/CoRN/ftc/MoreFunSeries/contg.var.
245 inline cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con.
247 inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con.
249 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con.
251 inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con.
253 inline cic:/CoRN/ftc/MoreFunSeries/F.var.
255 inline cic:/CoRN/ftc/MoreFunSeries/G.var.
257 inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
259 inline cic:/CoRN/ftc/MoreFunSeries/contG.var.
263 inline cic:/CoRN/ftc/MoreFunSeries/convF.var.
265 inline cic:/CoRN/ftc/MoreFunSeries/convG.var.
269 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con.
271 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con.
273 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con.
276 End Algebraic_Properties.
280 Section More_Algebraic_Properties.
284 If we work with the limit function things fit in just as well.
287 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
289 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
291 inline cic:/CoRN/ftc/MoreFunSeries/g.var.
293 inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
295 inline cic:/CoRN/ftc/MoreFunSeries/contg.var.
299 inline cic:/CoRN/ftc/MoreFunSeries/Hf.var.
301 inline cic:/CoRN/ftc/MoreFunSeries/Hg.var.
305 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con.
307 inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con.
309 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con.
311 inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con.
313 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con.
315 inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con.
317 inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con.
319 inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con.
322 End More_Algebraic_Properties.
329 (*#* ***Miscellaneous
331 Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
334 inline cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con.
336 inline cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con.
339 Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
342 inline cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con.
349 Section Series_Definitions.
354 We now consider series of functions defined in arbitrary intervals.
356 Convergence is defined as expected---through convergence in every compact interval.
359 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
361 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
363 inline cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con.
365 inline cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con.
369 inline cic:/CoRN/ftc/MoreFunSeries/H.var.
373 inline cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con.
375 (*#* Assume [h(x)] is the pointwise series of [f(x)] *)
379 inline cic:/CoRN/ftc/MoreFunSeries/h.con.
383 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con.
385 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con.
387 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con.
390 End Series_Definitions.
394 Implicit Arguments FSeries_Sum [J f].
398 Section More_Series_Definitions.
401 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
403 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
406 Absolute convergence still exists.
409 inline cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con.
412 End More_Series_Definitions.
416 Section Convergence_Results.
420 As before, any series converges to its sum.
423 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
425 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
427 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con.
429 inline cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con.
431 inline cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con.
433 inline cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con.
436 End Convergence_Results.
440 Hint Resolve convergent_imp_inc: included.
444 Hint Resolve convergent_imp_Continuous Continuous_FSeries_Sum: continuous.
451 (*#* **Algebraic Operations
453 Convergence is well defined and preserved by operations.
456 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
458 inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con.
460 inline cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con.
462 inline cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con.
464 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con.
466 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
468 inline cic:/CoRN/ftc/MoreFunSeries/g.var.
470 inline cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con.
474 inline cic:/CoRN/ftc/MoreFunSeries/convF.var.
476 inline cic:/CoRN/ftc/MoreFunSeries/convG.var.
480 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con.
482 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con.
484 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con.
486 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con.
488 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con.
490 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con.
492 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con.
495 %\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
499 inline cic:/CoRN/ftc/MoreFunSeries/c.var.
501 inline cic:/CoRN/ftc/MoreFunSeries/H.var.
503 inline cic:/CoRN/ftc/MoreFunSeries/contH.var.
505 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con.
507 inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con.
514 Section Convergence_Criteria.
517 (*#* ***Convergence Criteria
519 The most important tests for convergence of series still apply: the
520 comparison test (in both versions) and the ratio test.
523 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
525 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
527 inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
529 inline cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con.
531 inline cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con.
533 inline cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con.
535 inline cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con.
538 End Convergence_Criteria.
542 Section Insert_Series.
547 When working in particular with power series and Taylor series, it is
548 sometimes useful to ``shift'' all the terms in the series one position
549 forward, that is, replacing each $f_{i+1}$#f<sub>i+1</sub># with
550 $f_i$#f<sub>i</sub># and inserting the null function in the first
551 position. This does not affect convergence or the sum of the series.
554 inline cic:/CoRN/ftc/MoreFunSeries/J.var.
556 inline cic:/CoRN/ftc/MoreFunSeries/f.var.
558 inline cic:/CoRN/ftc/MoreFunSeries/convF.var.
560 inline cic:/CoRN/ftc/MoreFunSeries/insert_series.con.
562 inline cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con.
564 inline cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con.
566 inline cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con.
568 inline cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con.