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