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
53 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Definitions/a.var".
55 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Definitions/b.var".
57 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Definitions/Hab.var".
61 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/I.con" "Definitions__".
65 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Definitions/f.var".
67 alias id "F" = "cic:/CoRN/ftc/FunctSequence/Definitions/F.var".
69 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Definitions/contf.var".
71 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/Definitions/contF.var".
75 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/incf.con" "Definitions__".
77 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/incF.con" "Definitions__".
81 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con".
83 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con".
85 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con".
87 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con".
89 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con".
91 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con".
94 These definitions are all shown to be equivalent.
97 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con".
99 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con".
101 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con".
103 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con".
105 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con".
107 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con".
109 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con".
111 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con".
113 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con".
115 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con".
117 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con".
120 A Cauchy sequence of functions is pointwise a Cauchy sequence.
123 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con".
130 Section More_Definitions
133 alias id "a" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/a.var".
135 alias id "b" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/b.var".
137 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/Hab.var".
141 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Definitions/I.con" "More_Definitions__".
145 alias id "f" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/f.var".
147 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/contf.var".
150 We can also say that [f] is simply convergent if it converges to some
151 continuous function. Notice that we do not quantify directly over
152 partial functions, for reasons which were already explained.
155 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con".
158 It is useful to extract the limit as a partial function:
163 alias id "H" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/H.var".
167 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con".
174 Section Irrelevance_of_Proofs
177 (*#* **Irrelevance of Proofs
179 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.
182 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/a.var".
184 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/b.var".
186 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/Hab.var".
190 inline procedural "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/I.con" "Irrelevance_of_Proofs__".
194 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/f.var".
198 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf.var".
200 alias id "contf0" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf0.var".
204 alias id "F" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/F.var".
208 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF.var".
210 alias id "contF0" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF0.var".
214 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con".
216 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con".
218 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con".
220 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con".
222 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con".
225 End Irrelevance_of_Proofs
229 Section More_Proof_Irrelevance
232 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con".
235 End More_Proof_Irrelevance
239 Section More_Properties
242 (*#* **Other Properties
244 Still more technical details---a convergent sequence converges to its
245 limit; the limit is a continuous function; and convergence is well
246 defined with respect to functional equality in the interval [[a,b]].
249 alias id "a" = "cic:/CoRN/ftc/FunctSequence/More_Properties/a.var".
251 alias id "b" = "cic:/CoRN/ftc/FunctSequence/More_Properties/b.var".
253 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/More_Properties/Hab.var".
257 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Properties/I.con" "More_Properties__".
261 alias id "f" = "cic:/CoRN/ftc/FunctSequence/More_Properties/f.var".
263 alias id "g" = "cic:/CoRN/ftc/FunctSequence/More_Properties/g.var".
267 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contf.var".
269 alias id "contf0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contf0.var".
271 alias id "contg" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contg.var".
273 alias id "contg0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contg0.var".
277 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con".
279 alias id "F" = "cic:/CoRN/ftc/FunctSequence/More_Properties/F.var".
281 alias id "G" = "cic:/CoRN/ftc/FunctSequence/More_Properties/G.var".
285 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contF.var".
287 alias id "contF0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contF0.var".
289 alias id "contG" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contG.var".
291 alias id "contG0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contG0.var".
295 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con".
297 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con".
299 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con".
301 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con".
303 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con".
305 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con".
307 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con".
309 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con".
312 More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
315 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con".
318 And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
321 inline procedural "cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con".
328 Hint Resolve Cauchy_cont_Lim: continuous.
332 Section Algebraic_Properties
335 (*#* **Algebraic Properties
337 We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
340 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/a.var".
342 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/b.var".
344 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/Hab.var".
348 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/I.con" "Algebraic_Properties__".
352 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/f.var".
354 alias id "g" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/g.var".
356 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contf.var".
358 alias id "contg" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contg.var".
361 First, the limit function is unique.
364 inline procedural "cic:/CoRN/ftc/FunctSequence/FLim_unique.con".
366 (*#* Constant sequences (not sequences of constant functions!) always converge.
369 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con".
371 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con".
374 We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
377 alias id "F" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/F.var".
379 alias id "G" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/G.var".
381 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contF.var".
383 alias id "contG" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contG.var".
387 alias id "convF" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convF.var".
389 alias id "convG" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convG.var".
395 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incf.con" "Algebraic_Properties__".
397 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incg.con" "Algebraic_Properties__".
399 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incF.con" "Algebraic_Properties__".
401 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incG.con" "Algebraic_Properties__".
405 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con".
407 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con".
409 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con".
412 End Algebraic_Properties
416 Section More_Algebraic_Properties
419 alias id "a" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/a.var".
421 alias id "b" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/b.var".
423 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hab.var".
427 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/I.con" "More_Algebraic_Properties__".
431 alias id "f" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/f.var".
433 alias id "g" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/g.var".
435 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contf.var".
437 alias id "contg" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contg.var".
440 The same is true if we don't make the limits explicit.
445 alias id "Hf" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hf.var".
447 alias id "Hg" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hg.var".
451 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con".
453 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con".
455 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con".
457 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con".
459 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con".
461 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con".
464 End More_Algebraic_Properties
468 Section Still_More_Algebraic_Properties
471 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/a.var".
473 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/b.var".
475 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hab.var".
479 inline procedural "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/I.con" "Still_More_Algebraic_Properties__".
483 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/f.var".
485 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/contf.var".
487 alias id "Hf" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hf.var".
490 As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
493 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con".
495 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con".
498 End Still_More_Algebraic_Properties
502 Hint Resolve Continuous_I_Sum Continuous_I_Sumx Continuous_I_Sum0: continuous.