helm/software/matita/contribs/CoRN-Procedural/ftc/FunctSequence.mma

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