]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/FunctSequence.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / FunctSequence.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSequence".
18
19 include "CoRN.ma".
20
21 (* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
22
23 include "ftc/Continuity.ma".
24
25 include "ftc/PartInterval.ma".
26
27 (* UNEXPORTED
28 Section Definitions
29 *)
30
31 (*#* *Sequences of Functions
32
33 In this file we define some more operators on functions, namely
34 sequences and limits.  These concepts are defined only for continuous
35 functions.
36
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.
42
43 %\end{convention}%
44
45 **Definitions
46
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
52 see Bishop 1967.
53 *)
54
55 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Definitions/a.var".
56
57 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Definitions/b.var".
58
59 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Definitions/Hab.var".
60
61 (* begin hide *)
62
63 inline "cic:/CoRN/ftc/FunctSequence/Definitions/I.con" "Definitions__".
64
65 (* end hide *)
66
67 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Definitions/f.var".
68
69 alias id "F" = "cic:/CoRN/ftc/FunctSequence/Definitions/F.var".
70
71 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Definitions/contf.var".
72
73 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/Definitions/contF.var".
74
75 (* begin hide *)
76
77 inline "cic:/CoRN/ftc/FunctSequence/Definitions/incf.con" "Definitions__".
78
79 inline "cic:/CoRN/ftc/FunctSequence/Definitions/incF.con" "Definitions__".
80
81 (* end hide *)
82
83 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con".
84
85 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con".
86
87 inline "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con".
88
89 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con".
90
91 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con".
92
93 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con".
94
95 (*#*
96 These definitions are all shown to be equivalent.
97 *)
98
99 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con".
100
101 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con".
102
103 inline "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con".
104
105 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con".
106
107 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con".
108
109 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con".
110
111 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con".
112
113 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con".
114
115 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con".
116
117 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con".
118
119 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con".
120
121 (*#*
122 A Cauchy sequence of functions is pointwise a Cauchy sequence.
123 *)
124
125 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con".
126
127 (* UNEXPORTED
128 End Definitions
129 *)
130
131 (* UNEXPORTED
132 Section More_Definitions
133 *)
134
135 alias id "a" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/a.var".
136
137 alias id "b" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/b.var".
138
139 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/Hab.var".
140
141 (* begin hide *)
142
143 inline "cic:/CoRN/ftc/FunctSequence/More_Definitions/I.con" "More_Definitions__".
144
145 (* end hide *)
146
147 alias id "f" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/f.var".
148
149 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/contf.var".
150
151 (*#*
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.
155 *)
156
157 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con".
158
159 (*#*
160 It is useful to extract the limit as a partial function:
161 *)
162
163 (* begin show *)
164
165 alias id "H" = "cic:/CoRN/ftc/FunctSequence/More_Definitions/H.var".
166
167 (* end show *)
168
169 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con".
170
171 (* UNEXPORTED
172 End More_Definitions
173 *)
174
175 (* UNEXPORTED
176 Section Irrelevance_of_Proofs
177 *)
178
179 (*#* **Irrelevance of Proofs
180
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.
182 *)
183
184 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/a.var".
185
186 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/b.var".
187
188 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/Hab.var".
189
190 (* begin hide *)
191
192 inline "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/I.con" "Irrelevance_of_Proofs__".
193
194 (* end hide *)
195
196 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/f.var".
197
198 (* begin show *)
199
200 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf.var".
201
202 alias id "contf0" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf0.var".
203
204 (* end show *)
205
206 alias id "F" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/F.var".
207
208 (* begin show *)
209
210 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF.var".
211
212 alias id "contF0" = "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF0.var".
213
214 (* end show *)
215
216 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con".
217
218 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con".
219
220 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con".
221
222 inline "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con".
223
224 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con".
225
226 (* UNEXPORTED
227 End Irrelevance_of_Proofs
228 *)
229
230 (* UNEXPORTED
231 Section More_Proof_Irrelevance
232 *)
233
234 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con".
235
236 (* UNEXPORTED
237 End More_Proof_Irrelevance
238 *)
239
240 (* UNEXPORTED
241 Section More_Properties
242 *)
243
244 (*#* **Other Properties
245
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]].
249 *)
250
251 alias id "a" = "cic:/CoRN/ftc/FunctSequence/More_Properties/a.var".
252
253 alias id "b" = "cic:/CoRN/ftc/FunctSequence/More_Properties/b.var".
254
255 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/More_Properties/Hab.var".
256
257 (* begin hide *)
258
259 inline "cic:/CoRN/ftc/FunctSequence/More_Properties/I.con" "More_Properties__".
260
261 (* end hide *)
262
263 alias id "f" = "cic:/CoRN/ftc/FunctSequence/More_Properties/f.var".
264
265 alias id "g" = "cic:/CoRN/ftc/FunctSequence/More_Properties/g.var".
266
267 (* begin show *)
268
269 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contf.var".
270
271 alias id "contf0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contf0.var".
272
273 alias id "contg" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contg.var".
274
275 alias id "contg0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contg0.var".
276
277 (* end show *)
278
279 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con".
280
281 alias id "F" = "cic:/CoRN/ftc/FunctSequence/More_Properties/F.var".
282
283 alias id "G" = "cic:/CoRN/ftc/FunctSequence/More_Properties/G.var".
284
285 (* begin show *)
286
287 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contF.var".
288
289 alias id "contF0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contF0.var".
290
291 alias id "contG" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contG.var".
292
293 alias id "contG0" = "cic:/CoRN/ftc/FunctSequence/More_Properties/contG0.var".
294
295 (* end show *)
296
297 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con".
298
299 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con".
300
301 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con".
302
303 inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con".
304
305 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con".
306
307 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con".
308
309 inline "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con".
310
311 inline "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con".
312
313 (*#*
314 More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
315 *)
316
317 inline "cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con".
318
319 (*#*
320 And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
321 *)
322
323 inline "cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con".
324
325 (* UNEXPORTED
326 End More_Properties
327 *)
328
329 (* UNEXPORTED
330 Hint Resolve Cauchy_cont_Lim: continuous.
331 *)
332
333 (* UNEXPORTED
334 Section Algebraic_Properties
335 *)
336
337 (*#* **Algebraic Properties
338
339 We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
340 *)
341
342 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/a.var".
343
344 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/b.var".
345
346 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/Hab.var".
347
348 (* begin hide *)
349
350 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/I.con" "Algebraic_Properties__".
351
352 (* end hide *)
353
354 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/f.var".
355
356 alias id "g" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/g.var".
357
358 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contf.var".
359
360 alias id "contg" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contg.var".
361
362 (*#*
363 First, the limit function is unique.
364 *)
365
366 inline "cic:/CoRN/ftc/FunctSequence/FLim_unique.con".
367
368 (*#* Constant sequences (not sequences of constant functions!) always converge.
369 *)
370
371 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con".
372
373 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con".
374
375 (*#*
376 We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
377 *)
378
379 alias id "F" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/F.var".
380
381 alias id "G" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/G.var".
382
383 alias id "contF" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contF.var".
384
385 alias id "contG" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contG.var".
386
387 (* begin show *)
388
389 alias id "convF" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convF.var".
390
391 alias id "convG" = "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convG.var".
392
393 (* end show *)
394
395 (* begin hide *)
396
397 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incf.con" "Algebraic_Properties__".
398
399 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incg.con" "Algebraic_Properties__".
400
401 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incF.con" "Algebraic_Properties__".
402
403 inline "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incG.con" "Algebraic_Properties__".
404
405 (* end hide *)
406
407 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con".
408
409 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con".
410
411 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con".
412
413 (* UNEXPORTED
414 End Algebraic_Properties
415 *)
416
417 (* UNEXPORTED
418 Section More_Algebraic_Properties
419 *)
420
421 alias id "a" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/a.var".
422
423 alias id "b" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/b.var".
424
425 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hab.var".
426
427 (* begin hide *)
428
429 inline "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/I.con" "More_Algebraic_Properties__".
430
431 (* end hide *)
432
433 alias id "f" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/f.var".
434
435 alias id "g" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/g.var".
436
437 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contf.var".
438
439 alias id "contg" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contg.var".
440
441 (*#*
442 The same is true if we don't make the limits explicit.
443 *)
444
445 (* begin hide *)
446
447 alias id "Hf" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hf.var".
448
449 alias id "Hg" = "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hg.var".
450
451 (* end hide *)
452
453 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con".
454
455 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con".
456
457 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con".
458
459 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con".
460
461 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con".
462
463 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con".
464
465 (* UNEXPORTED
466 End More_Algebraic_Properties
467 *)
468
469 (* UNEXPORTED
470 Section Still_More_Algebraic_Properties
471 *)
472
473 alias id "a" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/a.var".
474
475 alias id "b" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/b.var".
476
477 alias id "Hab" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hab.var".
478
479 (* begin hide *)
480
481 inline "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/I.con" "Still_More_Algebraic_Properties__".
482
483 (* end hide *)
484
485 alias id "f" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/f.var".
486
487 alias id "contf" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/contf.var".
488
489 alias id "Hf" = "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hf.var".
490
491 (*#*
492 As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
493 *)
494
495 inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con".
496
497 inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con".
498
499 (* UNEXPORTED
500 End Still_More_Algebraic_Properties
501 *)
502
503 (* UNEXPORTED
504 Hint Resolve Continuous_I_Sum Continuous_I_Sumx Continuous_I_Sum0: continuous.
505 *)
506