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_notation.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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
  56
  57 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
  58
  59 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
  60
  61 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
  62
  63 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
  98
  99 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 100
 101 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
 102
 103 (* begin show *)
 104
 105 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 127
 128 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 129
 130 (* begin show *)
 131
 132 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
 133
 134 inline "cic:/CoRN/ftc/MoreFunSeries/contf0.var".
 135
 136 (* end show *)
 137
 138 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
 139
 140 (* begin show *)
 141
 142 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
 143
 144 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 167
 168 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 169
 170 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
 171
 172 (* begin show *)
 173
 174 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
 175
 176 inline "cic:/CoRN/ftc/MoreFunSeries/contf0.var".
 177
 178 inline "cic:/CoRN/ftc/MoreFunSeries/contg.var".
 179
 180 inline "cic:/CoRN/ftc/MoreFunSeries/contg0.var".
 181
 182 (* end show *)
 183
 184 inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con".
 185
 186 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
 187
 188 inline "cic:/CoRN/ftc/MoreFunSeries/G.var".
 189
 190 (* begin show *)
 191
 192 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
 193
 194 inline "cic:/CoRN/ftc/MoreFunSeries/contF0.var".
 195
 196 inline "cic:/CoRN/ftc/MoreFunSeries/contG.var".
 197
 198 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 234
 235 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 236
 237 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
 238
 239 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
 240
 241 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/F.var".
 252
 253 inline "cic:/CoRN/ftc/MoreFunSeries/G.var".
 254
 255 inline "cic:/CoRN/ftc/MoreFunSeries/contF.var".
 256
 257 inline "cic:/CoRN/ftc/MoreFunSeries/contG.var".
 258
 259 (* begin show *)
 260
 261 inline "cic:/CoRN/ftc/MoreFunSeries/convF.var".
 262
 263 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 286
 287 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 288
 289 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
 290
 291 inline "cic:/CoRN/ftc/MoreFunSeries/contf.var".
 292
 293 inline "cic:/CoRN/ftc/MoreFunSeries/contg.var".
 294
 295 (* begin show *)
 296
 297 inline "cic:/CoRN/ftc/MoreFunSeries/Hf.var".
 298
 299 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 358
 359 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/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/h.con".
 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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 400
 401 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 422
 423 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 465
 466 inline "cic:/CoRN/ftc/MoreFunSeries/g.var".
 467
 468 inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con".
 469
 470 (* begin show *)
 471
 472 inline "cic:/CoRN/ftc/MoreFunSeries/convF.var".
 473
 474 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/c.var".
 498
 499 inline "cic:/CoRN/ftc/MoreFunSeries/H.var".
 500
 501 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 522
 523 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 524
 525 inline "cic:/CoRN/ftc/MoreFunSeries/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 inline "cic:/CoRN/ftc/MoreFunSeries/J.var".
 553
 554 inline "cic:/CoRN/ftc/MoreFunSeries/f.var".
 555
 556 inline "cic:/CoRN/ftc/MoreFunSeries/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