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/FunctSequence".
21 (* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
23 include "ftc/Continuity.ma".
25 include "ftc/PartInterval.ma".
31 (*#* *Sequences of Functions
33 In this file we define some more operators on functions, namely
34 sequences and limits. These concepts are defined only for continuous
37 %\begin{convention}% Throughout this section:
38 - [a] and [b] will be real numbers and the interval [[a,b]]
39 will be denoted by [I];
40 - [f, g] and [h] will denote sequences of continuous functions;
41 - [F, G] and [H] will denote continuous functions.
47 A sequence of functions is simply an object of type [nat->PartIR].
48 However, we will be interested mostly in convergent and Cauchy
49 sequences. Several definitions of these concepts will be formalized;
50 they mirror the several different ways in which a Cauchy sequence can
51 be defined. For a discussion on the different notions of convergent
55 inline "cic:/CoRN/ftc/FunctSequence/Definitions/a.var" "Definitions__".
57 inline "cic:/CoRN/ftc/FunctSequence/Definitions/b.var" "Definitions__".
59 inline "cic:/CoRN/ftc/FunctSequence/Definitions/Hab.var" "Definitions__".
63 inline "cic:/CoRN/ftc/FunctSequence/Definitions/I.con" "Definitions__".
67 inline "cic:/CoRN/ftc/FunctSequence/Definitions/f.var" "Definitions__".
69 inline "cic:/CoRN/ftc/FunctSequence/Definitions/F.var" "Definitions__".
71 inline "cic:/CoRN/ftc/FunctSequence/Definitions/contf.var" "Definitions__".
73 inline "cic:/CoRN/ftc/FunctSequence/Definitions/contF.var" "Definitions__".
77 inline "cic:/CoRN/ftc/FunctSequence/Definitions/incf.con" "Definitions__".
79 inline "cic:/CoRN/ftc/FunctSequence/Definitions/incF.con" "Definitions__".
83 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con".
85 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con".
87 inline "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con".
89 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con".
91 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con".
93 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con".
96 These definitions are all shown to be equivalent.
99 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con".
101 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con".
103 inline "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con".
105 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con".
107 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con".
109 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con".
111 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con".
113 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con".
115 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con".
117 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con".
119 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con".
122 A Cauchy sequence of functions is pointwise a Cauchy sequence.
125 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con".
132 Section More_Definitions
135 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/a.var" "More_Definitions__".
137 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/b.var" "More_Definitions__".
139 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/Hab.var" "More_Definitions__".
143 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/I.con" "More_Definitions__".
147 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/f.var" "More_Definitions__".
149 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/contf.var" "More_Definitions__".
152 We can also say that [f] is simply convergent if it converges to some
153 continuous function. Notice that we do not quantify directly over
154 partial functions, for reasons which were already explained.
157 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con".
160 It is useful to extract the limit as a partial function:
165 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/H.var" "More_Definitions__".
169 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con".
176 Section Irrelevance_of_Proofs
179 (*#* **Irrelevance of Proofs
181 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.
184 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/a.var" "Irrelevance_of_Proofs__".
186 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/b.var" "Irrelevance_of_Proofs__".
188 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/Hab.var" "Irrelevance_of_Proofs__".
192 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/I.con" "Irrelevance_of_Proofs__".
196 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/f.var" "Irrelevance_of_Proofs__".
200 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf.var" "Irrelevance_of_Proofs__".
202 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf0.var" "Irrelevance_of_Proofs__".
206 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/F.var" "Irrelevance_of_Proofs__".
210 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF.var" "Irrelevance_of_Proofs__".
212 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF0.var" "Irrelevance_of_Proofs__".
216 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con".
218 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con".
220 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con".
222 inline "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con".
224 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con".
227 End Irrelevance_of_Proofs
231 Section More_Proof_Irrelevance
234 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con".
237 End More_Proof_Irrelevance
241 Section More_Properties
244 (*#* **Other Properties
246 Still more technical details---a convergent sequence converges to its
247 limit; the limit is a continuous function; and convergence is well
248 defined with respect to functional equality in the interval [[a,b]].
251 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/a.var" "More_Properties__".
253 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/b.var" "More_Properties__".
255 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/Hab.var" "More_Properties__".
259 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/I.con" "More_Properties__".
263 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/f.var" "More_Properties__".
265 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/g.var" "More_Properties__".
269 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contf.var" "More_Properties__".
271 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contf0.var" "More_Properties__".
273 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contg.var" "More_Properties__".
275 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contg0.var" "More_Properties__".
279 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con".
281 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/F.var" "More_Properties__".
283 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/G.var" "More_Properties__".
287 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contF.var" "More_Properties__".
289 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contF0.var" "More_Properties__".
291 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contG.var" "More_Properties__".
293 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/contG0.var" "More_Properties__".
297 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con".
299 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con".
301 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con".
303 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con".
305 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con".
307 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con".
309 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con".
311 inline "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con".
314 More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
317 inline "cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con".
320 And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
323 inline "cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con".
330 Hint Resolve Cauchy_cont_Lim: continuous.
334 Section Algebraic_Properties
337 (*#* **Algebraic Properties
339 We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
342 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/a.var" "Algebraic_Properties__".
344 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/b.var" "Algebraic_Properties__".
346 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/Hab.var" "Algebraic_Properties__".
350 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/I.con" "Algebraic_Properties__".
354 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/f.var" "Algebraic_Properties__".
356 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/g.var" "Algebraic_Properties__".
358 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contf.var" "Algebraic_Properties__".
360 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contg.var" "Algebraic_Properties__".
363 First, the limit function is unique.
366 inline "cic:/CoRN/ftc/FunctSequence/FLim_unique.con".
368 (*#* Constant sequences (not sequences of constant functions!) always converge.
371 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con".
373 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con".
376 We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
379 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/F.var" "Algebraic_Properties__".
381 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/G.var" "Algebraic_Properties__".
383 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contF.var" "Algebraic_Properties__".
385 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contG.var" "Algebraic_Properties__".
389 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convF.var" "Algebraic_Properties__".
391 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convG.var" "Algebraic_Properties__".
397 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incf.con" "Algebraic_Properties__".
399 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incg.con" "Algebraic_Properties__".
401 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incF.con" "Algebraic_Properties__".
403 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incG.con" "Algebraic_Properties__".
407 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con".
409 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con".
411 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con".
414 End Algebraic_Properties
418 Section More_Algebraic_Properties
421 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/a.var" "More_Algebraic_Properties__".
423 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/b.var" "More_Algebraic_Properties__".
425 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hab.var" "More_Algebraic_Properties__".
429 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/I.con" "More_Algebraic_Properties__".
433 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/f.var" "More_Algebraic_Properties__".
435 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/g.var" "More_Algebraic_Properties__".
437 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contf.var" "More_Algebraic_Properties__".
439 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contg.var" "More_Algebraic_Properties__".
442 The same is true if we don't make the limits explicit.
447 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hf.var" "More_Algebraic_Properties__".
449 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hg.var" "More_Algebraic_Properties__".
453 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con".
455 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con".
457 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con".
459 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con".
461 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con".
463 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con".
466 End More_Algebraic_Properties
470 Section Still_More_Algebraic_Properties
473 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/a.var" "Still_More_Algebraic_Properties__".
475 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/b.var" "Still_More_Algebraic_Properties__".
477 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hab.var" "Still_More_Algebraic_Properties__".
481 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/I.con" "Still_More_Algebraic_Properties__".
485 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/f.var" "Still_More_Algebraic_Properties__".
487 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/contf.var" "Still_More_Algebraic_Properties__".
489 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hf.var" "Still_More_Algebraic_Properties__".
492 As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
495 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con".
497 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con".
500 End Still_More_Algebraic_Properties
504 Hint Resolve Continuous_I_Sum Continuous_I_Sumx Continuous_I_Sum0: continuous.