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: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
21 include "ftc/Continuity.ma".
23 include "ftc/PartInterval.ma".
29 (*#* *Sequences of Functions
31 In this file we define some more operators on functions, namely
32 sequences and limits. These concepts are defined only for continuous
35 %\begin{convention}% Throughout this section:
36 - [a] and [b] will be real numbers and the interval [[a,b]]
37 will be denoted by [I];
38 - [f, g] and [h] will denote sequences of continuous functions;
39 - [F, G] and [H] will denote continuous functions.
45 A sequence of functions is simply an object of type [nat->PartIR].
46 However, we will be interested mostly in convergent and Cauchy
47 sequences. Several definitions of these concepts will be formalized;
48 they mirror the several different ways in which a Cauchy sequence can
49 be defined. For a discussion on the different notions of convergent
54 cic:/CoRN/ftc/FunctSequence/Definitions/a.var
58 cic:/CoRN/ftc/FunctSequence/Definitions/b.var
62 cic:/CoRN/ftc/FunctSequence/Definitions/Hab.var
67 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/I.con" "Definitions__" as definition.
72 cic:/CoRN/ftc/FunctSequence/Definitions/f.var
76 cic:/CoRN/ftc/FunctSequence/Definitions/F.var
80 cic:/CoRN/ftc/FunctSequence/Definitions/contf.var
84 cic:/CoRN/ftc/FunctSequence/Definitions/contF.var
89 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/incf.con" "Definitions__" as definition.
91 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/incF.con" "Definitions__" as definition.
95 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con" as definition.
97 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con" as definition.
99 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con" as definition.
101 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con" as definition.
103 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con" as definition.
105 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con" as definition.
108 These definitions are all shown to be equivalent.
111 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con" as lemma.
113 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con" as lemma.
115 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con" as lemma.
117 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con" as lemma.
119 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con" as lemma.
121 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con" as lemma.
123 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con" as lemma.
125 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con" as lemma.
127 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con" as lemma.
129 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con" as lemma.
131 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con" as lemma.
134 A Cauchy sequence of functions is pointwise a Cauchy sequence.
137 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con" as lemma.
144 Section More_Definitions
148 cic:/CoRN/ftc/FunctSequence/More_Definitions/a.var
152 cic:/CoRN/ftc/FunctSequence/More_Definitions/b.var
156 cic:/CoRN/ftc/FunctSequence/More_Definitions/Hab.var
161 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Definitions/I.con" "More_Definitions__" as definition.
166 cic:/CoRN/ftc/FunctSequence/More_Definitions/f.var
170 cic:/CoRN/ftc/FunctSequence/More_Definitions/contf.var
174 We can also say that [f] is simply convergent if it converges to some
175 continuous function. Notice that we do not quantify directly over
176 partial functions, for reasons which were already explained.
179 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con" as definition.
182 It is useful to extract the limit as a partial function:
188 cic:/CoRN/ftc/FunctSequence/More_Definitions/H.var
193 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con" as definition.
200 Section Irrelevance_of_Proofs
203 (*#* **Irrelevance of Proofs
205 This section contains a number of technical results stating mainly that being a Cauchy sequence or converging to some limit is a property of the sequence itself and independent of the proofs we supply of its continuity or the continuity of its limit.
209 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/a.var
213 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/b.var
217 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/Hab.var
222 inline procedural "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/I.con" "Irrelevance_of_Proofs__" as definition.
227 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/f.var
233 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf.var
237 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf0.var
243 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/F.var
249 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF.var
253 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF0.var
258 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con" as lemma.
260 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con" as lemma.
262 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con" as lemma.
264 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con" as lemma.
266 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con" as lemma.
269 End Irrelevance_of_Proofs
273 Section More_Proof_Irrelevance
276 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con" as lemma.
279 End More_Proof_Irrelevance
283 Section More_Properties
286 (*#* **Other Properties
288 Still more technical details---a convergent sequence converges to its
289 limit; the limit is a continuous function; and convergence is well
290 defined with respect to functional equality in the interval [[a,b]].
294 cic:/CoRN/ftc/FunctSequence/More_Properties/a.var
298 cic:/CoRN/ftc/FunctSequence/More_Properties/b.var
302 cic:/CoRN/ftc/FunctSequence/More_Properties/Hab.var
307 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Properties/I.con" "More_Properties__" as definition.
312 cic:/CoRN/ftc/FunctSequence/More_Properties/f.var
316 cic:/CoRN/ftc/FunctSequence/More_Properties/g.var
322 cic:/CoRN/ftc/FunctSequence/More_Properties/contf.var
326 cic:/CoRN/ftc/FunctSequence/More_Properties/contf0.var
330 cic:/CoRN/ftc/FunctSequence/More_Properties/contg.var
334 cic:/CoRN/ftc/FunctSequence/More_Properties/contg0.var
339 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con" as lemma.
342 cic:/CoRN/ftc/FunctSequence/More_Properties/F.var
346 cic:/CoRN/ftc/FunctSequence/More_Properties/G.var
352 cic:/CoRN/ftc/FunctSequence/More_Properties/contF.var
356 cic:/CoRN/ftc/FunctSequence/More_Properties/contF0.var
360 cic:/CoRN/ftc/FunctSequence/More_Properties/contG.var
364 cic:/CoRN/ftc/FunctSequence/More_Properties/contG0.var
369 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con" as lemma.
371 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con" as lemma.
373 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con" as lemma.
375 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con" as lemma.
377 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con" as lemma.
379 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con" as lemma.
381 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con" as lemma.
383 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con" as lemma.
386 More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
389 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con" as lemma.
392 And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
395 inline procedural "cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con" as lemma.
402 Hint Resolve Cauchy_cont_Lim: continuous.
406 Section Algebraic_Properties
409 (*#* **Algebraic Properties
411 We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
415 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/a.var
419 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/b.var
423 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/Hab.var
428 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/I.con" "Algebraic_Properties__" as definition.
433 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/f.var
437 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/g.var
441 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contf.var
445 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contg.var
449 First, the limit function is unique.
452 inline procedural "cic:/CoRN/ftc/FunctSequence/FLim_unique.con" as lemma.
454 (*#* Constant sequences (not sequences of constant functions!) always converge.
457 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con" as lemma.
459 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con" as lemma.
462 We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
466 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/F.var
470 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/G.var
474 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contF.var
478 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contG.var
484 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convF.var
488 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convG.var
495 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incf.con" "Algebraic_Properties__" as definition.
497 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incg.con" "Algebraic_Properties__" as definition.
499 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incF.con" "Algebraic_Properties__" as definition.
501 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incG.con" "Algebraic_Properties__" as definition.
505 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con" as lemma.
507 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con" as lemma.
509 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con" as lemma.
512 End Algebraic_Properties
516 Section More_Algebraic_Properties
520 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/a.var
524 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/b.var
528 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hab.var
533 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/I.con" "More_Algebraic_Properties__" as definition.
538 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/f.var
542 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/g.var
546 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contf.var
550 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contg.var
554 The same is true if we don't make the limits explicit.
560 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hf.var
564 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hg.var
569 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con" as lemma.
571 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con" as lemma.
573 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con" as lemma.
575 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con" as lemma.
577 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con" as lemma.
579 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con" as lemma.
582 End More_Algebraic_Properties
586 Section Still_More_Algebraic_Properties
590 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/a.var
594 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/b.var
598 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hab.var
603 inline procedural "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/I.con" "Still_More_Algebraic_Properties__" as definition.
608 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/f.var
612 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/contf.var
616 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hf.var
620 As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
623 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con" as lemma.
625 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con" as lemma.
628 End Still_More_Algebraic_Properties
632 Hint Resolve Continuous_I_Sum Continuous_I_Sumx Continuous_I_Sum0: continuous.