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