matita/contribs/CoRN-Decl/reals/Series.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/reals/Series".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: Series.v,v 1.6 2004/04/23 10:01:05 lcf Exp $ *)
  22
  23 (*#* printing seq_part_sum %\ensuremath{\sum^n}% #&sum;<sup>n</sup># *)
  24
  25 (*#* printing series_sum %\ensuremath{\sum_0^{\infty}}% #&sum;<sub>0</sub><sup>&infin;</sup># *)
  26
  27 (*#* printing pi %\ensuremath{\pi}% #&pi; *)
  28
  29 include "reals/CSumsReals.ma".
  30
  31 include "reals/NRootIR.ma".
  32
  33 (* UNEXPORTED
  34 Section Definitions
  35 *)
  36
  37 (*#* *Series of Real Numbers
  38 In this file we develop a theory of series of real numbers.
  39 ** Definitions
  40
  41 A series is simply a sequence from the natural numbers into the reals.
  42 To each such sequence we can assign a sequence of partial sums.
  43
  44 %\begin{convention}% Let [x:nat->IR].
  45 %\end{convention}%
  46 *)
  47
  48 alias id "x" = "cic:/CoRN/reals/Series/Definitions/x.var".
  49
  50 inline "cic:/CoRN/reals/Series/seq_part_sum.con".
  51
  52 (*#*
  53 For subsequent purposes it will be very useful to be able to write the
  54 difference between two arbitrary elements of the sequence of partial
  55 sums as a sum of elements of the original sequence.
  56 *)
  57
  58 inline "cic:/CoRN/reals/Series/seq_part_sum_n.con".
  59
  60 (*#* A series is convergent iff its sequence of partial Sums is a
  61 Cauchy sequence.  To each convergent series we can assign a Sum.
  62 *)
  63
  64 inline "cic:/CoRN/reals/Series/convergent.con".
  65
  66 inline "cic:/CoRN/reals/Series/series_sum.con".
  67
  68 (*#* Divergence can be characterized in a positive way, which will sometimes
  69 be useful.  We thus define divergence of sequences and series and prove the
  70 obvious fact that no sequence can be both convergent and divergent, whether
  71  considered either as a sequence or as a series.
  72 *)
  73
  74 inline "cic:/CoRN/reals/Series/divergent_seq.con".
  75
  76 inline "cic:/CoRN/reals/Series/divergent.con".
  77
  78 inline "cic:/CoRN/reals/Series/conv_imp_not_div.con".
  79
  80 inline "cic:/CoRN/reals/Series/div_imp_not_conv.con".
  81
  82 inline "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con".
  83
  84 inline "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con".
  85
  86 (*#* Finally we have the well known fact that every convergent series converges
  87 to zero as a sequence.
  88 *)
  89
  90 inline "cic:/CoRN/reals/Series/series_seq_Lim.con".
  91
  92 inline "cic:/CoRN/reals/Series/series_seq_Lim'.con".
  93
  94 (* UNEXPORTED
  95 End Definitions
  96 *)
  97
  98 (* UNEXPORTED
  99 Section More_Definitions
 100 *)
 101
 102 alias id "x" = "cic:/CoRN/reals/Series/More_Definitions/x.var".
 103
 104 (*#* We also define absolute convergence. *)
 105
 106 inline "cic:/CoRN/reals/Series/abs_convergent.con".
 107
 108 (* UNEXPORTED
 109 End More_Definitions
 110 *)
 111
 112 (* UNEXPORTED
 113 Section Power_Series
 114 *)
 115
 116 (*#* **Power Series
 117
 118 Power series are an important special case.
 119 *)
 120
 121 inline "cic:/CoRN/reals/Series/power_series.con".
 122
 123 (*#*
 124 Specially important is the case when [c] is a positive real number
 125 less than 1; in this case not only the power series is convergent, but
 126 we can also compute its sum.
 127
 128 %\begin{convention}% Let [c] be a real number between 0 and 1.
 129 %\end{convention}%
 130 *)
 131
 132 alias id "c" = "cic:/CoRN/reals/Series/Power_Series/c.var".
 133
 134 alias id "H0c" = "cic:/CoRN/reals/Series/Power_Series/H0c.var".
 135
 136 alias id "Hc1" = "cic:/CoRN/reals/Series/Power_Series/Hc1.var".
 137
 138 inline "cic:/CoRN/reals/Series/c_exp_Lim.con".
 139
 140 inline "cic:/CoRN/reals/Series/power_series_Lim1.con".
 141
 142 inline "cic:/CoRN/reals/Series/power_series_conv.con".
 143
 144 inline "cic:/CoRN/reals/Series/power_series_sum.con".
 145
 146 (* UNEXPORTED
 147 End Power_Series
 148 *)
 149
 150 (* UNEXPORTED
 151 Section Operations
 152 *)
 153
 154 (*#* **Operations
 155
 156 Some operations with series preserve convergence.  We start by defining
 157 the series that is zero everywhere.
 158 *)
 159
 160 inline "cic:/CoRN/reals/Series/conv_zero_series.con".
 161
 162 inline "cic:/CoRN/reals/Series/series_sum_zero.con".
 163
 164 (*#* Next we consider extensionality, as well as the sum and difference
 165 of two convergent series.
 166
 167 %\begin{convention}% Let [x,y:nat->IR] be convergent series.
 168 %\end{convention}%
 169 *)
 170
 171 alias id "x" = "cic:/CoRN/reals/Series/Operations/x.var".
 172
 173 alias id "y" = "cic:/CoRN/reals/Series/Operations/y.var".
 174
 175 alias id "convX" = "cic:/CoRN/reals/Series/Operations/convX.var".
 176
 177 alias id "convY" = "cic:/CoRN/reals/Series/Operations/convY.var".
 178
 179 inline "cic:/CoRN/reals/Series/convergent_wd.con".
 180
 181 inline "cic:/CoRN/reals/Series/series_sum_wd.con".
 182
 183 inline "cic:/CoRN/reals/Series/conv_series_plus.con".
 184
 185 inline "cic:/CoRN/reals/Series/series_sum_plus.con".
 186
 187 inline "cic:/CoRN/reals/Series/conv_series_minus.con".
 188
 189 inline "cic:/CoRN/reals/Series/series_sum_minus.con".
 190
 191 (*#* Multiplication by a scalar [c] is also permitted. *)
 192
 193 alias id "c" = "cic:/CoRN/reals/Series/Operations/c.var".
 194
 195 inline "cic:/CoRN/reals/Series/conv_series_mult_scal.con".
 196
 197 inline "cic:/CoRN/reals/Series/series_sum_mult_scal.con".
 198
 199 (* UNEXPORTED
 200 End Operations
 201 *)
 202
 203 (* UNEXPORTED
 204 Section More_Operations
 205 *)
 206
 207 alias id "x" = "cic:/CoRN/reals/Series/More_Operations/x.var".
 208
 209 alias id "convX" = "cic:/CoRN/reals/Series/More_Operations/convX.var".
 210
 211 (*#* As a corollary, we get the series of the inverses. *)
 212
 213 inline "cic:/CoRN/reals/Series/conv_series_inv.con".
 214
 215 inline "cic:/CoRN/reals/Series/series_sum_inv.con".
 216
 217 (* UNEXPORTED
 218 End More_Operations
 219 *)
 220
 221 (* UNEXPORTED
 222 Section Almost_Everywhere
 223 *)
 224
 225 (*#* ** Almost Everywhere
 226
 227 In this section we strengthen some of the convergence results for sequences
 228 and derive an important corollary for series.
 229
 230 Let [x,y : nat->IR] be equal after some natural number.
 231 *)
 232
 233 alias id "x" = "cic:/CoRN/reals/Series/Almost_Everywhere/x.var".
 234
 235 alias id "y" = "cic:/CoRN/reals/Series/Almost_Everywhere/y.var".
 236
 237 inline "cic:/CoRN/reals/Series/aew_eq.con".
 238
 239 alias id "aew_equal" = "cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var".
 240
 241 inline "cic:/CoRN/reals/Series/aew_Cauchy.con".
 242
 243 inline "cic:/CoRN/reals/Series/aew_Cauchy2.con".
 244
 245 inline "cic:/CoRN/reals/Series/aew_series_conv.con".
 246
 247 (* UNEXPORTED
 248 End Almost_Everywhere
 249 *)
 250
 251 (* UNEXPORTED
 252 Section Cauchy_Almost_Everywhere
 253 *)
 254
 255 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
 256
 257 alias id "x" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var".
 258
 259 alias id "y" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var".
 260
 261 alias id "aew_equal" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var".
 262
 263 inline "cic:/CoRN/reals/Series/aew_Lim.con".
 264
 265 (* UNEXPORTED
 266 End Cauchy_Almost_Everywhere
 267 *)
 268
 269 (* UNEXPORTED
 270 Section Convergence_Criteria
 271 *)
 272
 273 (*#* **Convergence Criteria
 274
 275 %\begin{convention}% Let [x:nat->IR].
 276 %\end{convention}%
 277 *)
 278
 279 alias id "x" = "cic:/CoRN/reals/Series/Convergence_Criteria/x.var".
 280
 281 (*#* We include the comparison test for series, both in a strong and in a less
 282 general (but simpler) form.
 283 *)
 284
 285 inline "cic:/CoRN/reals/Series/str_comparison.con".
 286
 287 inline "cic:/CoRN/reals/Series/comparison.con".
 288
 289 (*#* As a corollary, we get that every absolutely convergent series converges. *)
 290
 291 inline "cic:/CoRN/reals/Series/abs_imp_conv.con".
 292
 293 (*#* Next we have the ratio test, both as a positive and negative result. *)
 294
 295 inline "cic:/CoRN/reals/Series/divergent_crit.con".
 296
 297 inline "cic:/CoRN/reals/Series/tail_series.con".
 298
 299 inline "cic:/CoRN/reals/Series/join_series.con".
 300
 301 (* UNEXPORTED
 302 End Convergence_Criteria
 303 *)
 304
 305 (* UNEXPORTED
 306 Section More_CC
 307 *)
 308
 309 alias id "x" = "cic:/CoRN/reals/Series/More_CC/x.var".
 310
 311 inline "cic:/CoRN/reals/Series/ratio_test_conv.con".
 312
 313 inline "cic:/CoRN/reals/Series/ratio_test_div.con".
 314
 315 (* UNEXPORTED
 316 End More_CC
 317 *)
 318
 319 (* UNEXPORTED
 320 Section Alternate_Series
 321 *)
 322
 323 (*#* **Alternate Series
 324
 325 Alternate series are a special case.  Suppose that [x] is nonnegative and
 326 decreasing convergent to 0.
 327 *)
 328
 329 alias id "x" = "cic:/CoRN/reals/Series/Alternate_Series/x.var".
 330
 331 alias id "pos_x" = "cic:/CoRN/reals/Series/Alternate_Series/pos_x.var".
 332
 333 alias id "Lim_x" = "cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var".
 334
 335 alias id "mon_x" = "cic:/CoRN/reals/Series/Alternate_Series/mon_x.var".
 336
 337 (* begin hide *)
 338
 339 inline "cic:/CoRN/reals/Series/Alternate_Series/y.con" "Alternate_Series__".
 340
 341 inline "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma1.con" "Alternate_Series__".
 342
 343 inline "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma2.con" "Alternate_Series__".
 344
 345 inline "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma3.con" "Alternate_Series__".
 346
 347 inline "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma4.con" "Alternate_Series__".
 348
 349 (* end hide *)
 350
 351 inline "cic:/CoRN/reals/Series/alternate_series_conv.con".
 352
 353 (* UNEXPORTED
 354 End Alternate_Series
 355 *)
 356
 357 (* UNEXPORTED
 358 Section Important_Numbers
 359 *)
 360
 361 (*#* **Important Numbers
 362
 363 We end this chapter by defining two important numbers in mathematics: [pi]
 364 and $e$#e#, both as sums of convergent series.
 365 *)
 366
 367 inline "cic:/CoRN/reals/Series/e_series.con".
 368
 369 inline "cic:/CoRN/reals/Series/e_series_conv.con".
 370
 371 inline "cic:/CoRN/reals/Series/E.con".
 372
 373 inline "cic:/CoRN/reals/Series/pi_series.con".
 374
 375 inline "cic:/CoRN/reals/Series/pi_series_conv.con".
 376
 377 inline "cic:/CoRN/reals/Series/pi.con".
 378
 379 (* UNEXPORTED
 380 End Important_Numbers
 381 *)
 382