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".
19 (* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
33 (*#* *Sequences of Functions
35 In this file we define some more operators on functions, namely
36 sequences and limits. These concepts are defined only for continuous
39 %\begin{convention}% Throughout this section:
40 - [a] and [b] will be real numbers and the interval [[a,b]]
41 will be denoted by [I];
42 - [f, g] and [h] will denote sequences of continuous functions;
43 - [F, G] and [H] will denote continuous functions.
49 A sequence of functions is simply an object of type [nat->PartIR].
50 However, we will be interested mostly in convergent and Cauchy
51 sequences. Several definitions of these concepts will be formalized;
52 they mirror the several different ways in which a Cauchy sequence can
53 be defined. For a discussion on the different notions of convergent
57 inline cic:/CoRN/ftc/FunctSequence/a.var.
59 inline cic:/CoRN/ftc/FunctSequence/b.var.
61 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
65 inline cic:/CoRN/ftc/FunctSequence/I.con.
69 inline cic:/CoRN/ftc/FunctSequence/f.var.
71 inline cic:/CoRN/ftc/FunctSequence/F.var.
73 inline cic:/CoRN/ftc/FunctSequence/contf.var.
75 inline cic:/CoRN/ftc/FunctSequence/contF.var.
79 inline cic:/CoRN/ftc/FunctSequence/incf.con.
81 inline cic:/CoRN/ftc/FunctSequence/incF.con.
85 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con.
87 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con.
89 inline cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con.
91 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con.
93 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con.
95 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con.
98 These definitions are all shown to be equivalent.
101 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con.
103 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con.
105 inline cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con.
107 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con.
109 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con.
111 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con.
113 inline cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con.
115 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con.
117 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con.
119 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con.
121 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con.
124 A Cauchy sequence of functions is pointwise a Cauchy sequence.
127 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con.
134 Section More_Definitions.
137 inline cic:/CoRN/ftc/FunctSequence/a.var.
139 inline cic:/CoRN/ftc/FunctSequence/b.var.
141 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
145 inline cic:/CoRN/ftc/FunctSequence/I.con.
149 inline cic:/CoRN/ftc/FunctSequence/f.var.
151 inline cic:/CoRN/ftc/FunctSequence/contf.var.
154 We can also say that [f] is simply convergent if it converges to some
155 continuous function. Notice that we do not quantify directly over
156 partial functions, for reasons which were already explained.
159 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con.
162 It is useful to extract the limit as a partial function:
167 inline cic:/CoRN/ftc/FunctSequence/H.var.
171 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con.
174 End More_Definitions.
178 Section Irrelevance_of_Proofs.
181 (*#* **Irrelevance of Proofs
183 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.
186 inline cic:/CoRN/ftc/FunctSequence/a.var.
188 inline cic:/CoRN/ftc/FunctSequence/b.var.
190 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
194 inline cic:/CoRN/ftc/FunctSequence/I.con.
198 inline cic:/CoRN/ftc/FunctSequence/f.var.
202 inline cic:/CoRN/ftc/FunctSequence/contf.var.
204 inline cic:/CoRN/ftc/FunctSequence/contf0.var.
208 inline cic:/CoRN/ftc/FunctSequence/F.var.
212 inline cic:/CoRN/ftc/FunctSequence/contF.var.
214 inline cic:/CoRN/ftc/FunctSequence/contF0.var.
218 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con.
220 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con.
222 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con.
224 inline cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con.
226 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con.
229 End Irrelevance_of_Proofs.
233 Section More_Proof_Irrelevance.
236 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con.
239 End More_Proof_Irrelevance.
243 Section More_Properties.
246 (*#* **Other Properties
248 Still more technical details---a convergent sequence converges to its
249 limit; the limit is a continuous function; and convergence is well
250 defined with respect to functional equality in the interval [[a,b]].
253 inline cic:/CoRN/ftc/FunctSequence/a.var.
255 inline cic:/CoRN/ftc/FunctSequence/b.var.
257 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
261 inline cic:/CoRN/ftc/FunctSequence/I.con.
265 inline cic:/CoRN/ftc/FunctSequence/f.var.
267 inline cic:/CoRN/ftc/FunctSequence/g.var.
271 inline cic:/CoRN/ftc/FunctSequence/contf.var.
273 inline cic:/CoRN/ftc/FunctSequence/contf0.var.
275 inline cic:/CoRN/ftc/FunctSequence/contg.var.
277 inline cic:/CoRN/ftc/FunctSequence/contg0.var.
281 inline cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con.
283 inline cic:/CoRN/ftc/FunctSequence/F.var.
285 inline cic:/CoRN/ftc/FunctSequence/G.var.
289 inline cic:/CoRN/ftc/FunctSequence/contF.var.
291 inline cic:/CoRN/ftc/FunctSequence/contF0.var.
293 inline cic:/CoRN/ftc/FunctSequence/contG.var.
295 inline cic:/CoRN/ftc/FunctSequence/contG0.var.
299 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con.
301 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con.
303 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con.
305 inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con.
307 inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con.
309 inline cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con.
311 inline cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con.
313 inline cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con.
316 More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
319 inline cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con.
322 And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
325 inline cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con.
332 Hint Resolve Cauchy_cont_Lim: continuous.
336 Section Algebraic_Properties.
339 (*#* **Algebraic Properties
341 We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
344 inline cic:/CoRN/ftc/FunctSequence/a.var.
346 inline cic:/CoRN/ftc/FunctSequence/b.var.
348 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
352 inline cic:/CoRN/ftc/FunctSequence/I.con.
356 inline cic:/CoRN/ftc/FunctSequence/f.var.
358 inline cic:/CoRN/ftc/FunctSequence/g.var.
360 inline cic:/CoRN/ftc/FunctSequence/contf.var.
362 inline cic:/CoRN/ftc/FunctSequence/contg.var.
365 First, the limit function is unique.
368 inline cic:/CoRN/ftc/FunctSequence/FLim_unique.con.
370 (*#* Constant sequences (not sequences of constant functions!) always converge.
373 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con.
375 inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con.
378 We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
381 inline cic:/CoRN/ftc/FunctSequence/F.var.
383 inline cic:/CoRN/ftc/FunctSequence/G.var.
385 inline cic:/CoRN/ftc/FunctSequence/contF.var.
387 inline cic:/CoRN/ftc/FunctSequence/contG.var.
391 inline cic:/CoRN/ftc/FunctSequence/convF.var.
393 inline cic:/CoRN/ftc/FunctSequence/convG.var.
399 inline cic:/CoRN/ftc/FunctSequence/incf.con.
401 inline cic:/CoRN/ftc/FunctSequence/incg.con.
403 inline cic:/CoRN/ftc/FunctSequence/incF.con.
405 inline cic:/CoRN/ftc/FunctSequence/incG.con.
409 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con.
411 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con.
413 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con.
416 End Algebraic_Properties.
420 Section More_Algebraic_Properties.
423 inline cic:/CoRN/ftc/FunctSequence/a.var.
425 inline cic:/CoRN/ftc/FunctSequence/b.var.
427 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
431 inline cic:/CoRN/ftc/FunctSequence/I.con.
435 inline cic:/CoRN/ftc/FunctSequence/f.var.
437 inline cic:/CoRN/ftc/FunctSequence/g.var.
439 inline cic:/CoRN/ftc/FunctSequence/contf.var.
441 inline cic:/CoRN/ftc/FunctSequence/contg.var.
444 The same is true if we don't make the limits explicit.
449 inline cic:/CoRN/ftc/FunctSequence/Hf.var.
451 inline cic:/CoRN/ftc/FunctSequence/Hg.var.
455 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con.
457 inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con.
459 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con.
461 inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con.
463 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con.
465 inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con.
468 End More_Algebraic_Properties.
472 Section Still_More_Algebraic_Properties.
475 inline cic:/CoRN/ftc/FunctSequence/a.var.
477 inline cic:/CoRN/ftc/FunctSequence/b.var.
479 inline cic:/CoRN/ftc/FunctSequence/Hab.var.
483 inline cic:/CoRN/ftc/FunctSequence/I.con.
487 inline cic:/CoRN/ftc/FunctSequence/f.var.
489 inline cic:/CoRN/ftc/FunctSequence/contf.var.
491 inline cic:/CoRN/ftc/FunctSequence/Hf.var.
494 As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
497 inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con.
499 inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con.
502 End Still_More_Algebraic_Properties.
506 Hint Resolve Continuous_I_Sum Continuous_I_Sumx Continuous_I_Sum0: continuous.