helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma

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