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