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