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 inline "cic:/CoRN/ftc/FunctSeries/a.var".
  57
  58 inline "cic:/CoRN/ftc/FunctSeries/b.var".
  59
  60 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
  61
  62 (* begin hide *)
  63
  64 inline "cic:/CoRN/ftc/FunctSeries/I.con".
  65
  66 (* end hide *)
  67
  68 inline "cic:/CoRN/ftc/FunctSeries/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 inline "cic:/CoRN/ftc/FunctSeries/H.var".
  91
  92 (* end show *)
  93
  94 (* begin hide *)
  95
  96 inline "cic:/CoRN/ftc/FunctSeries/contf.con".
  97
  98 inline "cic:/CoRN/ftc/FunctSeries/incf.con".
  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 inline "cic:/CoRN/ftc/FunctSeries/a.var".
 123
 124 inline "cic:/CoRN/ftc/FunctSeries/b.var".
 125
 126 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
 127
 128 inline "cic:/CoRN/ftc/FunctSeries/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 inline "cic:/CoRN/ftc/FunctSeries/a.var".
 148
 149 inline "cic:/CoRN/ftc/FunctSeries/b.var".
 150
 151 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
 152
 153 (* begin hide *)
 154
 155 inline "cic:/CoRN/ftc/FunctSeries/I.con".
 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 inline "cic:/CoRN/ftc/FunctSeries/f.var".
 172
 173 inline "cic:/CoRN/ftc/FunctSeries/g.var".
 174
 175 (* end show *)
 176
 177 inline "cic:/CoRN/ftc/FunctSeries/fun_series_convergent_wd.con".
 178
 179 (* begin show *)
 180
 181 inline "cic:/CoRN/ftc/FunctSeries/convF.var".
 182
 183 inline "cic:/CoRN/ftc/FunctSeries/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 inline "cic:/CoRN/ftc/FunctSeries/c.var".
 203
 204 inline "cic:/CoRN/ftc/FunctSeries/H.var".
 205
 206 inline "cic:/CoRN/ftc/FunctSeries/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 inline "cic:/CoRN/ftc/FunctSeries/a.var".
 221
 222 inline "cic:/CoRN/ftc/FunctSeries/b.var".
 223
 224 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
 225
 226 (* begin hide *)
 227
 228 inline "cic:/CoRN/ftc/FunctSeries/I.con".
 229
 230 (* end hide *)
 231
 232 inline "cic:/CoRN/ftc/FunctSeries/f.var".
 233
 234 inline "cic:/CoRN/ftc/FunctSeries/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 inline "cic:/CoRN/ftc/FunctSeries/a.var".
 249
 250 inline "cic:/CoRN/ftc/FunctSeries/b.var".
 251
 252 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
 253
 254 inline "cic:/CoRN/ftc/FunctSeries/f.var".
 255
 256 inline "cic:/CoRN/ftc/FunctSeries/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 inline "cic:/CoRN/ftc/FunctSeries/a.var".
 292
 293 inline "cic:/CoRN/ftc/FunctSeries/b.var".
 294
 295 inline "cic:/CoRN/ftc/FunctSeries/Hab.var".
 296
 297 (* begin hide *)
 298
 299 inline "cic:/CoRN/ftc/FunctSeries/I.con".
 300
 301 (* end hide *)
 302
 303 inline "cic:/CoRN/ftc/FunctSeries/f.var".
 304
 305 inline "cic:/CoRN/ftc/FunctSeries/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