matita/contribs/CoRN-Decl/ftc/MoreFunSeries.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/MoreFunSeries".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
  22
  23 include "ftc/FunctSeries.ma".
  24
  25 include "ftc/MoreFunctions.ma".
  26
  27 (*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #&sum;'<sub>&infin;</sub># *)
  28
  29 (* UNEXPORTED
  30 Section Definitions
  31 *)
  32
  33 (*#* *More on Sequences and Series
  34
  35 We will now extend our convergence definitions and results for
  36 sequences and series of functions defined in compact intervals to
  37 arbitrary intervals.
  38
  39 %\begin{convention}% Throughout this file, [J] will be an interval,
  40 [f, g] will be sequences of continuous (in [J]) functions and [F,G]
  41 will be continuous (in [J]) functions.
  42 %\end{convention}%
  43
  44 **Sequences
  45
  46 First we will consider the case of sequences.
  47
  48 ***Definitions
  49
  50 Some of the definitions do not make sense in this more general setting
  51 (for instance, because the norm of a function is no longer defined),
  52 but the ones which do we simply adapt in the usual way.
  53 *)
  54
  55 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/J.var".
  56
  57 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/f.var".
  58
  59 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/F.var".
  60
  61 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contf.var".
  62
  63 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contF.var".
  64
  65 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con".
  66
  67 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con".
  68
  69 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con".
  70
  71 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con".
  72
  73 (*#*
  74 The equivalences between these definitions still hold.
  75 *)
  76
  77 inline "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con".
  78
  79 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con".
  80
  81 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con".
  82
  83 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con".
  84
  85 (* UNEXPORTED
  86 End Definitions
  87 *)
  88
  89 (* UNEXPORTED
  90 Section More_Definitions
  91 *)
  92
  93 (*#*
  94 Limit is defined and works in the same way as before.
  95 *)
  96
  97 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/J.var".
  98
  99 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/f.var".
 100
 101 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/contf.var".
 102
 103 (* begin show *)
 104
 105 alias id "conv" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/conv.var".
 106
 107 (* end show *)
 108
 109 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con".
 110
 111 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con".
 112
 113 (* UNEXPORTED
 114 End More_Definitions
 115 *)
 116
 117 (* UNEXPORTED
 118 Section Irrelevance_of_Proofs
 119 *)
 120
 121 (*#* ***Basic Properties
 122
 123 Proofs are irrelevant as before---they just have to be present.
 124 *)
 125
 126 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/J.var".
 127
 128 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/f.var".
 129
 130 (* begin show *)
 131
 132 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf.var".
 133
 134 alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf0.var".
 135
 136 (* end show *)
 137
 138 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/F.var".
 139
 140 (* begin show *)
 141
 142 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF.var".
 143
 144 alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF0.var".
 145
 146 (* end show *)
 147
 148 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con".
 149
 150 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con".
 151
 152 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con".
 153
 154 (* UNEXPORTED
 155 End Irrelevance_of_Proofs
 156 *)
 157
 158 (* UNEXPORTED
 159 Opaque Cauchy_fun_seq_Lim_IR.
 160 *)
 161
 162 (* UNEXPORTED
 163 Section More_Properties
 164 *)
 165
 166 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/J.var".
 167
 168 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/f.var".
 169
 170 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/g.var".
 171
 172 (* begin show *)
 173
 174 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf.var".
 175
 176 alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf0.var".
 177
 178 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg.var".
 179
 180 alias id "contg0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg0.var".
 181
 182 (* end show *)
 183
 184 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con".
 185
 186 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/F.var".
 187
 188 alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/G.var".
 189
 190 (* begin show *)
 191
 192 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF.var".
 193
 194 alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF0.var".
 195
 196 alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG.var".
 197
 198 alias id "contG0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG0.var".
 199
 200 (* end show *)
 201
 202 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con".
 203
 204 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con".
 205
 206 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con".
 207
 208 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con".
 209
 210 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con".
 211
 212 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con".
 213
 214 inline "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con".
 215
 216 (* UNEXPORTED
 217 End More_Properties
 218 *)
 219
 220 (* UNEXPORTED
 221 Hint Resolve Cauchy_cont_Lim_IR: continuous.
 222 *)
 223
 224 (* UNEXPORTED
 225 Section Algebraic_Properties
 226 *)
 227
 228 (*#* ***Algebraic Properties
 229
 230 Algebraic operations still work well.
 231 *)
 232
 233 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/J.var".
 234
 235 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/f.var".
 236
 237 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/g.var".
 238
 239 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contf.var".
 240
 241 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contg.var".
 242
 243 inline "cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con".
 244
 245 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con".
 246
 247 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con".
 248
 249 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con".
 250
 251 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/F.var".
 252
 253 alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/G.var".
 254
 255 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contF.var".
 256
 257 alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contG.var".
 258
 259 (* begin show *)
 260
 261 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convF.var".
 262
 263 alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convG.var".
 264
 265 (* end show *)
 266
 267 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con".
 268
 269 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con".
 270
 271 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con".
 272
 273 (* UNEXPORTED
 274 End Algebraic_Properties
 275 *)
 276
 277 (* UNEXPORTED
 278 Section More_Algebraic_Properties
 279 *)
 280
 281 (*#*
 282 If we work with the limit function things fit in just as well.
 283 *)
 284
 285 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/J.var".
 286
 287 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/f.var".
 288
 289 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/g.var".
 290
 291 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contf.var".
 292
 293 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contg.var".
 294
 295 (* begin show *)
 296
 297 alias id "Hf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hf.var".
 298
 299 alias id "Hg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hg.var".
 300
 301 (* end show *)
 302
 303 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con".
 304
 305 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con".
 306
 307 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con".
 308
 309 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con".
 310
 311 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con".
 312
 313 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con".
 314
 315 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con".
 316
 317 inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con".
 318
 319 (* UNEXPORTED
 320 End More_Algebraic_Properties
 321 *)
 322
 323 (* UNEXPORTED
 324 Section Other
 325 *)
 326
 327 (*#* ***Miscellaneous
 328
 329 Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
 330 *)
 331
 332 inline "cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con".
 333
 334 inline "cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con".
 335
 336 (*#*
 337 Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
 338 *)
 339
 340 inline "cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con".
 341
 342 (* UNEXPORTED
 343 End Other
 344 *)
 345
 346 (* UNEXPORTED
 347 Section Series_Definitions
 348 *)
 349
 350 (*#* **Series
 351
 352 We now consider series of functions defined in arbitrary intervals.
 353
 354 Convergence is defined as expected---through convergence in every compact interval.
 355 *)
 356
 357 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/J.var".
 358
 359 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/f.var".
 360
 361 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con".
 362
 363 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con".
 364
 365 (* begin show *)
 366
 367 alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/H.var".
 368
 369 (* end show *)
 370
 371 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con".
 372
 373 (*#* Assume [h(x)] is the pointwise series of [f(x)] *)
 374
 375 (* begin hide *)
 376
 377 inline "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/h.con" "Series_Definitions__".
 378
 379 (* end hide *)
 380
 381 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con".
 382
 383 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con".
 384
 385 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con".
 386
 387 (* UNEXPORTED
 388 End Series_Definitions
 389 *)
 390
 391 (* UNEXPORTED
 392 Implicit Arguments FSeries_Sum [J f].
 393 *)
 394
 395 (* UNEXPORTED
 396 Section More_Series_Definitions
 397 *)
 398
 399 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/J.var".
 400
 401 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/f.var".
 402
 403 (*#*
 404 Absolute convergence still exists.
 405 *)
 406
 407 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con".
 408
 409 (* UNEXPORTED
 410 End More_Series_Definitions
 411 *)
 412
 413 (* UNEXPORTED
 414 Section Convergence_Results
 415 *)
 416
 417 (*#*
 418 As before, any series converges to its sum.
 419 *)
 420
 421 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/J.var".
 422
 423 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/f.var".
 424
 425 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con".
 426
 427 inline "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con".
 428
 429 inline "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con".
 430
 431 inline "cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con".
 432
 433 (* UNEXPORTED
 434 End Convergence_Results
 435 *)
 436
 437 (* UNEXPORTED
 438 Hint Resolve convergent_imp_inc: included.
 439 *)
 440
 441 (* UNEXPORTED
 442 Hint Resolve convergent_imp_Continuous Continuous_FSeries_Sum: continuous.
 443 *)
 444
 445 (* UNEXPORTED
 446 Section Operations
 447 *)
 448
 449 (*#* **Algebraic Operations
 450
 451 Convergence is well defined and preserved by operations.
 452 *)
 453
 454 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Operations/J.var".
 455
 456 inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con".
 457
 458 inline "cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con".
 459
 460 inline "cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con".
 461
 462 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con".
 463
 464 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Operations/f.var".
 465
 466 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Operations/g.var".
 467
 468 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con".
 469
 470 (* begin show *)
 471
 472 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convF.var".
 473
 474 alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convG.var".
 475
 476 (* end show *)
 477
 478 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con".
 479
 480 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con".
 481
 482 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con".
 483
 484 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con".
 485
 486 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con".
 487
 488 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con".
 489
 490 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con".
 491
 492 (*#*
 493 %\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
 494 %\end{convention}%
 495 *)
 496
 497 alias id "c" = "cic:/CoRN/ftc/MoreFunSeries/Operations/c.var".
 498
 499 alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Operations/H.var".
 500
 501 alias id "contH" = "cic:/CoRN/ftc/MoreFunSeries/Operations/contH.var".
 502
 503 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con".
 504
 505 inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con".
 506
 507 (* UNEXPORTED
 508 End Operations
 509 *)
 510
 511 (* UNEXPORTED
 512 Section Convergence_Criteria
 513 *)
 514
 515 (*#* ***Convergence Criteria
 516
 517 The most important tests for convergence of series still apply: the
 518 comparison test (in both versions) and the ratio test.
 519 *)
 520
 521 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/J.var".
 522
 523 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/f.var".
 524
 525 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/contF.var".
 526
 527 inline "cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con".
 528
 529 inline "cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con".
 530
 531 inline "cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con".
 532
 533 inline "cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con".
 534
 535 (* UNEXPORTED
 536 End Convergence_Criteria
 537 *)
 538
 539 (* UNEXPORTED
 540 Section Insert_Series
 541 *)
 542
 543 (*#* ***Translation
 544
 545 When working in particular with power series and Taylor series, it is
 546 sometimes useful to ``shift'' all the terms in the series one position
 547 forward, that is, replacing each $f_{i+1}$#f<sub>i+1</sub># with
 548 $f_i$#f<sub>i</sub># and inserting the null function in the first
 549 position.  This does not affect convergence or the sum of the series.
 550 *)
 551
 552 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/J.var".
 553
 554 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/f.var".
 555
 556 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/convF.var".
 557
 558 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series.con".
 559
 560 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con".
 561
 562 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con".
 563
 564 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con".
 565
 566 inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con".
 567
 568 (* UNEXPORTED
 569 End Insert_Series
 570 *)
 571