helm/software/matita/contribs/procedural/CoRN/ftc/FunctSeries.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: FunctSeries.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 include "ftc/FunctSequence.ma".
  22
  23 include "reals/Series.ma".
  24
  25 (*#* printing fun_seq_part_sum %\ensuremath{\sum^n}% #&sum;<sup>n</sup># *)
  26
  27 (*#* printing Fun_Series_Sum %\ensuremath{\sum_0^{\infty}}% #&sum;<sub>0</sub><sup>&infin;</sup># *)
  28
  29 (* UNEXPORTED
  30 Section Definitions
  31 *)
  32
  33 (*#* *Series of Functions
  34
  35 We now turn our attention to series of functions.  Like it was already
  36 the case for sequences, we will mainly rewrite the results we proved
  37 for series of real numbers in a different way.
  38
  39 %\begin{convention}% Throughout this section:
  40  - [a] and [b] will be real numbers and the interval [[a,b]] will be denoted
  41 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 As before, we will consider only sequences of continuous functions
  50 defined in a compact interval.  For this, partial sums are defined and
  51 convergence is simply the convergence of the sequence of partial sums.
  52 *)
  53
  54 (* UNEXPORTED
  55 cic:/CoRN/ftc/FunctSeries/Definitions/a.var
  56 *)
  57
  58 (* UNEXPORTED
  59 cic:/CoRN/ftc/FunctSeries/Definitions/b.var
  60 *)
  61
  62 (* UNEXPORTED
  63 cic:/CoRN/ftc/FunctSeries/Definitions/Hab.var
  64 *)
  65
  66 (* begin hide *)
  67
  68 inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/I.con" "Definitions__" as definition.
  69
  70 (* end hide *)
  71
  72 (* UNEXPORTED
  73 cic:/CoRN/ftc/FunctSeries/Definitions/f.var
  74 *)
  75
  76 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum.con" as definition.
  77
  78 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_cont.con" as lemma.
  79
  80 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_convergent.con" as definition.
  81
  82 (*#*
  83 For what comes up next we need to know that the convergence of a
  84 series of functions implies pointwise convergence of the corresponding
  85 real number series.
  86 *)
  87
  88 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_conv_imp_conv.con" as lemma.
  89
  90 (*#* We then define the sum of the series as being the pointwise sum of
  91 the corresponding series.
  92 *)
  93
  94 (* begin show *)
  95
  96 (* UNEXPORTED
  97 cic:/CoRN/ftc/FunctSeries/Definitions/H.var
  98 *)
  99
 100 (* end show *)
 101
 102 (* begin hide *)
 103
 104 inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/contf.con" "Definitions__" as definition.
 105
 106 inline procedural "cic:/CoRN/ftc/FunctSeries/Definitions/incf.con" "Definitions__" as definition.
 107
 108 (* end hide *)
 109
 110 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_strext.con" as lemma.
 111
 112 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum.con" as definition.
 113
 114 (* UNEXPORTED
 115 End Definitions
 116 *)
 117
 118 (* UNEXPORTED
 119 Implicit Arguments Fun_Series_Sum [a b Hab f].
 120 *)
 121
 122 (* UNEXPORTED
 123 Hint Resolve fun_seq_part_sum_cont: continuous.
 124 *)
 125
 126 (* UNEXPORTED
 127 Section More_Definitions
 128 *)
 129
 130 (* UNEXPORTED
 131 cic:/CoRN/ftc/FunctSeries/More_Definitions/a.var
 132 *)
 133
 134 (* UNEXPORTED
 135 cic:/CoRN/ftc/FunctSeries/More_Definitions/b.var
 136 *)
 137
 138 (* UNEXPORTED
 139 cic:/CoRN/ftc/FunctSeries/More_Definitions/Hab.var
 140 *)
 141
 142 (* UNEXPORTED
 143 cic:/CoRN/ftc/FunctSeries/More_Definitions/f.var
 144 *)
 145
 146 (*#* A series can also be absolutely convergent. *)
 147
 148 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_abs_convergent.con" as definition.
 149
 150 (* UNEXPORTED
 151 End More_Definitions
 152 *)
 153
 154 (* UNEXPORTED
 155 Section Operations
 156 *)
 157
 158 (* **Algebraic Properties
 159
 160 All of these are analogous to the properties for series of real numbers, so we won't comment much about them.
 161 *)
 162
 163 (* UNEXPORTED
 164 cic:/CoRN/ftc/FunctSeries/Operations/a.var
 165 *)
 166
 167 (* UNEXPORTED
 168 cic:/CoRN/ftc/FunctSeries/Operations/b.var
 169 *)
 170
 171 (* UNEXPORTED
 172 cic:/CoRN/ftc/FunctSeries/Operations/Hab.var
 173 *)
 174
 175 (* begin hide *)
 176
 177 inline procedural "cic:/CoRN/ftc/FunctSeries/Operations/I.con" "Operations__" as definition.
 178
 179 (* end hide *)
 180
 181 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_n.con" as lemma.
 182
 183 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_const_series.con" as lemma.
 184
 185 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_const_series_sum.con" as lemma.
 186
 187 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_zero_fun_series.con" as lemma.
 188
 189 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_zero.con" as lemma.
 190
 191 (* begin show *)
 192
 193 (* UNEXPORTED
 194 cic:/CoRN/ftc/FunctSeries/Operations/f.var
 195 *)
 196
 197 (* UNEXPORTED
 198 cic:/CoRN/ftc/FunctSeries/Operations/g.var
 199 *)
 200
 201 (* end show *)
 202
 203 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con" as lemma.
 204
 205 (* begin show *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/ftc/FunctSeries/Operations/convF.var
 209 *)
 210
 211 (* UNEXPORTED
 212 cic:/CoRN/ftc/FunctSeries/Operations/convG.var
 213 *)
 214
 215 (* end show *)
 216
 217 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_wd'.con" as lemma.
 218
 219 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_plus.con" as lemma.
 220
 221 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_plus.con" as lemma.
 222
 223 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_minus.con" as lemma.
 224
 225 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_min.con" as lemma.
 226
 227 (*#*
 228 %\begin{convention}% Let [c:IR].
 229 %\end{convention}%
 230 *)
 231
 232 (* UNEXPORTED
 233 cic:/CoRN/ftc/FunctSeries/Operations/c.var
 234 *)
 235
 236 (* UNEXPORTED
 237 cic:/CoRN/ftc/FunctSeries/Operations/H.var
 238 *)
 239
 240 (* UNEXPORTED
 241 cic:/CoRN/ftc/FunctSeries/Operations/contH.var
 242 *)
 243
 244 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_scal.con" as lemma.
 245
 246 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_scal.con" as lemma.
 247
 248 (* UNEXPORTED
 249 End Operations
 250 *)
 251
 252 (* UNEXPORTED
 253 Section More_Operations
 254 *)
 255
 256 (* UNEXPORTED
 257 cic:/CoRN/ftc/FunctSeries/More_Operations/a.var
 258 *)
 259
 260 (* UNEXPORTED
 261 cic:/CoRN/ftc/FunctSeries/More_Operations/b.var
 262 *)
 263
 264 (* UNEXPORTED
 265 cic:/CoRN/ftc/FunctSeries/More_Operations/Hab.var
 266 *)
 267
 268 (* begin hide *)
 269
 270 inline procedural "cic:/CoRN/ftc/FunctSeries/More_Operations/I.con" "More_Operations__" as definition.
 271
 272 (* end hide *)
 273
 274 (* UNEXPORTED
 275 cic:/CoRN/ftc/FunctSeries/More_Operations/f.var
 276 *)
 277
 278 (* UNEXPORTED
 279 cic:/CoRN/ftc/FunctSeries/More_Operations/convF.var
 280 *)
 281
 282 inline procedural "cic:/CoRN/ftc/FunctSeries/conv_fun_series_inv.con" as lemma.
 283
 284 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_inv.con" as lemma.
 285
 286 (* UNEXPORTED
 287 End More_Operations
 288 *)
 289
 290 (* UNEXPORTED
 291 Section Other_Results
 292 *)
 293
 294 (* UNEXPORTED
 295 cic:/CoRN/ftc/FunctSeries/Other_Results/a.var
 296 *)
 297
 298 (* UNEXPORTED
 299 cic:/CoRN/ftc/FunctSeries/Other_Results/b.var
 300 *)
 301
 302 (* UNEXPORTED
 303 cic:/CoRN/ftc/FunctSeries/Other_Results/Hab.var
 304 *)
 305
 306 (* UNEXPORTED
 307 cic:/CoRN/ftc/FunctSeries/Other_Results/f.var
 308 *)
 309
 310 (* UNEXPORTED
 311 cic:/CoRN/ftc/FunctSeries/Other_Results/convF.var
 312 *)
 313
 314 (*#*
 315 The following relate the sum series with the limit of the sequence of
 316 partial sums; as a corollary we get the continuity of the sum of the
 317 series.
 318 *)
 319
 320 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char'.con" as lemma.
 321
 322 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_series_conv.con" as lemma.
 323
 324 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_cont.con" as lemma.
 325
 326 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char.con" as lemma.
 327
 328 inline procedural "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_as_Lim.con" as lemma.
 329
 330 (* UNEXPORTED
 331 End Other_Results
 332 *)
 333
 334 (* UNEXPORTED
 335 Hint Resolve Fun_Series_Sum_cont: continuous.
 336 *)
 337
 338 (* UNEXPORTED
 339 Section Convergence_Criteria
 340 *)
 341
 342 (*#* **Convergence Criteria
 343
 344 Most of the convergence criteria for series of real numbers carry over to series of real-valued functions, so again we just present them without comments.
 345 *)
 346
 347 (* UNEXPORTED
 348 cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/a.var
 349 *)
 350
 351 (* UNEXPORTED
 352 cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/b.var
 353 *)
 354
 355 (* UNEXPORTED
 356 cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/Hab.var
 357 *)
 358
 359 (* begin hide *)
 360
 361 inline procedural "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/I.con" "Convergence_Criteria__" as definition.
 362
 363 (* end hide *)
 364
 365 (* UNEXPORTED
 366 cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/f.var
 367 *)
 368
 369 (* UNEXPORTED
 370 cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/contF.var
 371 *)
 372
 373 (* UNEXPORTED
 374 Opaque Frestr.
 375 *)
 376
 377 (* UNEXPORTED
 378 Transparent Frestr.
 379 *)
 380
 381 (* UNEXPORTED
 382 Opaque FAbs.
 383 *)
 384
 385 (* UNEXPORTED
 386 Transparent FAbs.
 387 *)
 388
 389 (* UNEXPORTED
 390 Opaque fun_seq_part_sum.
 391 *)
 392
 393 (* UNEXPORTED
 394 Opaque FAbs.
 395 *)
 396
 397 (* UNEXPORTED
 398 Transparent FAbs.
 399 *)
 400
 401 (* UNEXPORTED
 402 Opaque FAbs.
 403 *)
 404
 405 (* UNEXPORTED
 406 Transparent fun_seq_part_sum.
 407 *)
 408
 409 (* UNEXPORTED
 410 Opaque fun_seq_part_sum.
 411 *)
 412
 413 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_str_comparison.con" as lemma.
 414
 415 (* UNEXPORTED
 416 Transparent FAbs.
 417 *)
 418
 419 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_comparison.con" as lemma.
 420
 421 inline procedural "cic:/CoRN/ftc/FunctSeries/abs_imp_conv.con" as lemma.
 422
 423 (* UNEXPORTED
 424 Opaque FAbs.
 425 *)
 426
 427 inline procedural "cic:/CoRN/ftc/FunctSeries/fun_ratio_test_conv.con" as lemma.
 428
 429 (* UNEXPORTED
 430 End Convergence_Criteria
 431 *)
 432