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