matita/matita/contribs/CoRN-Decl/ftc/FunctSeries.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 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 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Definitions/a.var".
  55
  56 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Definitions/b.var".
  57
  58 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Definitions/Hab.var".
  59
  60 (* begin hide *)
  61
  62 inline "cic:/CoRN/ftc/FunctSeries/Definitions/I.con" "Definitions__".
  63
  64 (* end hide *)
  65
  66 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Definitions/f.var".
  67
  68 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum.con".
  69
  70 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_cont.con".
  71
  72 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent.con".
  73
  74 (*#*
  75 For what comes up next we need to know that the convergence of a
  76 series of functions implies pointwise convergence of the corresponding
  77 real number series.
  78 *)
  79
  80 inline "cic:/CoRN/ftc/FunctSeries/fun_series_conv_imp_conv.con".
  81
  82 (*#* We then define the sum of the series as being the pointwise sum of
  83 the corresponding series.
  84 *)
  85
  86 (* begin show *)
  87
  88 alias id "H" = "cic:/CoRN/ftc/FunctSeries/Definitions/H.var".
  89
  90 (* end show *)
  91
  92 (* begin hide *)
  93
  94 inline "cic:/CoRN/ftc/FunctSeries/Definitions/contf.con" "Definitions__".
  95
  96 inline "cic:/CoRN/ftc/FunctSeries/Definitions/incf.con" "Definitions__".
  97
  98 (* end hide *)
  99
 100 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_strext.con".
 101
 102 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum.con".
 103
 104 (* UNEXPORTED
 105 End Definitions
 106 *)
 107
 108 (* UNEXPORTED
 109 Implicit Arguments Fun_Series_Sum [a b Hab f].
 110 *)
 111
 112 (* UNEXPORTED
 113 Hint Resolve fun_seq_part_sum_cont: continuous.
 114 *)
 115
 116 (* UNEXPORTED
 117 Section More_Definitions
 118 *)
 119
 120 alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/a.var".
 121
 122 alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/b.var".
 123
 124 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/Hab.var".
 125
 126 alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Definitions/f.var".
 127
 128 (*#* A series can also be absolutely convergent. *)
 129
 130 inline "cic:/CoRN/ftc/FunctSeries/fun_series_abs_convergent.con".
 131
 132 (* UNEXPORTED
 133 End More_Definitions
 134 *)
 135
 136 (* UNEXPORTED
 137 Section Operations
 138 *)
 139
 140 (* **Algebraic Properties
 141
 142 All of these are analogous to the properties for series of real numbers, so we won't comment much about them.
 143 *)
 144
 145 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Operations/a.var".
 146
 147 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Operations/b.var".
 148
 149 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Operations/Hab.var".
 150
 151 (* begin hide *)
 152
 153 inline "cic:/CoRN/ftc/FunctSeries/Operations/I.con" "Operations__".
 154
 155 (* end hide *)
 156
 157 inline "cic:/CoRN/ftc/FunctSeries/fun_seq_part_sum_n.con".
 158
 159 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_const_series.con".
 160
 161 inline "cic:/CoRN/ftc/FunctSeries/fun_const_series_sum.con".
 162
 163 inline "cic:/CoRN/ftc/FunctSeries/conv_zero_fun_series.con".
 164
 165 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_zero.con".
 166
 167 (* begin show *)
 168
 169 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Operations/f.var".
 170
 171 alias id "g" = "cic:/CoRN/ftc/FunctSeries/Operations/g.var".
 172
 173 (* end show *)
 174
 175 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con".
 176
 177 (* begin show *)
 178
 179 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Operations/convF.var".
 180
 181 alias id "convG" = "cic:/CoRN/ftc/FunctSeries/Operations/convG.var".
 182
 183 (* end show *)
 184
 185 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_wd'.con".
 186
 187 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_plus.con".
 188
 189 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_plus.con".
 190
 191 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_minus.con".
 192
 193 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_min.con".
 194
 195 (*#*
 196 %\begin{convention}% Let [c:IR].
 197 %\end{convention}%
 198 *)
 199
 200 alias id "c" = "cic:/CoRN/ftc/FunctSeries/Operations/c.var".
 201
 202 alias id "H" = "cic:/CoRN/ftc/FunctSeries/Operations/H.var".
 203
 204 alias id "contH" = "cic:/CoRN/ftc/FunctSeries/Operations/contH.var".
 205
 206 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_scal.con".
 207
 208 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_scal.con".
 209
 210 (* UNEXPORTED
 211 End Operations
 212 *)
 213
 214 (* UNEXPORTED
 215 Section More_Operations
 216 *)
 217
 218 alias id "a" = "cic:/CoRN/ftc/FunctSeries/More_Operations/a.var".
 219
 220 alias id "b" = "cic:/CoRN/ftc/FunctSeries/More_Operations/b.var".
 221
 222 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/More_Operations/Hab.var".
 223
 224 (* begin hide *)
 225
 226 inline "cic:/CoRN/ftc/FunctSeries/More_Operations/I.con" "More_Operations__".
 227
 228 (* end hide *)
 229
 230 alias id "f" = "cic:/CoRN/ftc/FunctSeries/More_Operations/f.var".
 231
 232 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/More_Operations/convF.var".
 233
 234 inline "cic:/CoRN/ftc/FunctSeries/conv_fun_series_inv.con".
 235
 236 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_inv.con".
 237
 238 (* UNEXPORTED
 239 End More_Operations
 240 *)
 241
 242 (* UNEXPORTED
 243 Section Other_Results
 244 *)
 245
 246 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Other_Results/a.var".
 247
 248 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Other_Results/b.var".
 249
 250 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Other_Results/Hab.var".
 251
 252 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Other_Results/f.var".
 253
 254 alias id "convF" = "cic:/CoRN/ftc/FunctSeries/Other_Results/convF.var".
 255
 256 (*#*
 257 The following relate the sum series with the limit of the sequence of
 258 partial sums; as a corollary we get the continuity of the sum of the
 259 series.
 260 *)
 261
 262 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char'.con".
 263
 264 inline "cic:/CoRN/ftc/FunctSeries/fun_series_conv.con".
 265
 266 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_cont.con".
 267
 268 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_char.con".
 269
 270 inline "cic:/CoRN/ftc/FunctSeries/Fun_Series_Sum_as_Lim.con".
 271
 272 (* UNEXPORTED
 273 End Other_Results
 274 *)
 275
 276 (* UNEXPORTED
 277 Hint Resolve Fun_Series_Sum_cont: continuous.
 278 *)
 279
 280 (* UNEXPORTED
 281 Section Convergence_Criteria
 282 *)
 283
 284 (*#* **Convergence Criteria
 285
 286 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.
 287 *)
 288
 289 alias id "a" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/a.var".
 290
 291 alias id "b" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/b.var".
 292
 293 alias id "Hab" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/Hab.var".
 294
 295 (* begin hide *)
 296
 297 inline "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/I.con" "Convergence_Criteria__".
 298
 299 (* end hide *)
 300
 301 alias id "f" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/f.var".
 302
 303 alias id "contF" = "cic:/CoRN/ftc/FunctSeries/Convergence_Criteria/contF.var".
 304
 305 (* UNEXPORTED
 306 Opaque Frestr.
 307 *)
 308
 309 (* UNEXPORTED
 310 Transparent Frestr.
 311 *)
 312
 313 (* UNEXPORTED
 314 Opaque FAbs.
 315 *)
 316
 317 (* UNEXPORTED
 318 Transparent FAbs.
 319 *)
 320
 321 (* UNEXPORTED
 322 Opaque fun_seq_part_sum.
 323 *)
 324
 325 (* UNEXPORTED
 326 Opaque FAbs.
 327 *)
 328
 329 (* UNEXPORTED
 330 Transparent FAbs.
 331 *)
 332
 333 (* UNEXPORTED
 334 Opaque FAbs.
 335 *)
 336
 337 (* UNEXPORTED
 338 Transparent fun_seq_part_sum.
 339 *)
 340
 341 (* UNEXPORTED
 342 Opaque fun_seq_part_sum.
 343 *)
 344
 345 inline "cic:/CoRN/ftc/FunctSeries/fun_str_comparison.con".
 346
 347 (* UNEXPORTED
 348 Transparent FAbs.
 349 *)
 350
 351 inline "cic:/CoRN/ftc/FunctSeries/fun_comparison.con".
 352
 353 inline "cic:/CoRN/ftc/FunctSeries/abs_imp_conv.con".
 354
 355 (* UNEXPORTED
 356 Opaque FAbs.
 357 *)
 358
 359 inline "cic:/CoRN/ftc/FunctSeries/fun_ratio_test_conv.con".
 360
 361 (* UNEXPORTED
 362 End Convergence_Criteria
 363 *)
 364