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