helm/software/matita/contribs/procedural/CoRN/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 (* UNEXPORTED
  47 cic:/CoRN/reals/Series/Definitions/x.var
  48 *)
  49
  50 inline procedural "cic:/CoRN/reals/Series/seq_part_sum.con" as definition.
  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 procedural "cic:/CoRN/reals/Series/seq_part_sum_n.con" as lemma.
  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 procedural "cic:/CoRN/reals/Series/convergent.con" as definition.
  65
  66 inline procedural "cic:/CoRN/reals/Series/series_sum.con" as definition.
  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 procedural "cic:/CoRN/reals/Series/divergent_seq.con" as definition.
  75
  76 inline procedural "cic:/CoRN/reals/Series/divergent.con" as definition.
  77
  78 inline procedural "cic:/CoRN/reals/Series/conv_imp_not_div.con" as lemma.
  79
  80 inline procedural "cic:/CoRN/reals/Series/div_imp_not_conv.con" as lemma.
  81
  82 inline procedural "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con" as lemma.
  83
  84 inline procedural "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con" as lemma.
  85
  86 (*#* Finally we have the well known fact that every convergent series converges
  87 to zero as a sequence.
  88 *)
  89
  90 inline procedural "cic:/CoRN/reals/Series/series_seq_Lim.con" as lemma.
  91
  92 inline procedural "cic:/CoRN/reals/Series/series_seq_Lim'.con" as lemma.
  93
  94 (* UNEXPORTED
  95 End Definitions
  96 *)
  97
  98 (* UNEXPORTED
  99 Section More_Definitions
 100 *)
 101
 102 (* UNEXPORTED
 103 cic:/CoRN/reals/Series/More_Definitions/x.var
 104 *)
 105
 106 (*#* We also define absolute convergence. *)
 107
 108 inline procedural "cic:/CoRN/reals/Series/abs_convergent.con" as definition.
 109
 110 (* UNEXPORTED
 111 End More_Definitions
 112 *)
 113
 114 (* UNEXPORTED
 115 Section Power_Series
 116 *)
 117
 118 (*#* **Power Series
 119
 120 Power series are an important special case.
 121 *)
 122
 123 inline procedural "cic:/CoRN/reals/Series/power_series.con" as definition.
 124
 125 (*#*
 126 Specially important is the case when [c] is a positive real number
 127 less than 1; in this case not only the power series is convergent, but
 128 we can also compute its sum.
 129
 130 %\begin{convention}% Let [c] be a real number between 0 and 1.
 131 %\end{convention}%
 132 *)
 133
 134 (* UNEXPORTED
 135 cic:/CoRN/reals/Series/Power_Series/c.var
 136 *)
 137
 138 (* UNEXPORTED
 139 cic:/CoRN/reals/Series/Power_Series/H0c.var
 140 *)
 141
 142 (* UNEXPORTED
 143 cic:/CoRN/reals/Series/Power_Series/Hc1.var
 144 *)
 145
 146 inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con" as lemma.
 147
 148 inline procedural "cic:/CoRN/reals/Series/power_series_Lim1.con" as lemma.
 149
 150 inline procedural "cic:/CoRN/reals/Series/power_series_conv.con" as lemma.
 151
 152 inline procedural "cic:/CoRN/reals/Series/power_series_sum.con" as lemma.
 153
 154 (* UNEXPORTED
 155 End Power_Series
 156 *)
 157
 158 (* UNEXPORTED
 159 Section Operations
 160 *)
 161
 162 (*#* **Operations
 163
 164 Some operations with series preserve convergence.  We start by defining
 165 the series that is zero everywhere.
 166 *)
 167
 168 inline procedural "cic:/CoRN/reals/Series/conv_zero_series.con" as lemma.
 169
 170 inline procedural "cic:/CoRN/reals/Series/series_sum_zero.con" as lemma.
 171
 172 (*#* Next we consider extensionality, as well as the sum and difference
 173 of two convergent series.
 174
 175 %\begin{convention}% Let [x,y:nat->IR] be convergent series.
 176 %\end{convention}%
 177 *)
 178
 179 (* UNEXPORTED
 180 cic:/CoRN/reals/Series/Operations/x.var
 181 *)
 182
 183 (* UNEXPORTED
 184 cic:/CoRN/reals/Series/Operations/y.var
 185 *)
 186
 187 (* UNEXPORTED
 188 cic:/CoRN/reals/Series/Operations/convX.var
 189 *)
 190
 191 (* UNEXPORTED
 192 cic:/CoRN/reals/Series/Operations/convY.var
 193 *)
 194
 195 inline procedural "cic:/CoRN/reals/Series/convergent_wd.con" as lemma.
 196
 197 inline procedural "cic:/CoRN/reals/Series/series_sum_wd.con" as lemma.
 198
 199 inline procedural "cic:/CoRN/reals/Series/conv_series_plus.con" as lemma.
 200
 201 inline procedural "cic:/CoRN/reals/Series/series_sum_plus.con" as lemma.
 202
 203 inline procedural "cic:/CoRN/reals/Series/conv_series_minus.con" as lemma.
 204
 205 inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con" as lemma.
 206
 207 (*#* Multiplication by a scalar [c] is also permitted. *)
 208
 209 (* UNEXPORTED
 210 cic:/CoRN/reals/Series/Operations/c.var
 211 *)
 212
 213 inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con" as lemma.
 214
 215 inline procedural "cic:/CoRN/reals/Series/series_sum_mult_scal.con" as lemma.
 216
 217 (* UNEXPORTED
 218 End Operations
 219 *)
 220
 221 (* UNEXPORTED
 222 Section More_Operations
 223 *)
 224
 225 (* UNEXPORTED
 226 cic:/CoRN/reals/Series/More_Operations/x.var
 227 *)
 228
 229 (* UNEXPORTED
 230 cic:/CoRN/reals/Series/More_Operations/convX.var
 231 *)
 232
 233 (*#* As a corollary, we get the series of the inverses. *)
 234
 235 inline procedural "cic:/CoRN/reals/Series/conv_series_inv.con" as lemma.
 236
 237 inline procedural "cic:/CoRN/reals/Series/series_sum_inv.con" as lemma.
 238
 239 (* UNEXPORTED
 240 End More_Operations
 241 *)
 242
 243 (* UNEXPORTED
 244 Section Almost_Everywhere
 245 *)
 246
 247 (*#* ** Almost Everywhere
 248
 249 In this section we strengthen some of the convergence results for sequences
 250 and derive an important corollary for series.
 251
 252 Let [x,y : nat->IR] be equal after some natural number.
 253 *)
 254
 255 (* UNEXPORTED
 256 cic:/CoRN/reals/Series/Almost_Everywhere/x.var
 257 *)
 258
 259 (* UNEXPORTED
 260 cic:/CoRN/reals/Series/Almost_Everywhere/y.var
 261 *)
 262
 263 inline procedural "cic:/CoRN/reals/Series/aew_eq.con" as definition.
 264
 265 (* UNEXPORTED
 266 cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var
 267 *)
 268
 269 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con" as lemma.
 270
 271 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy2.con" as lemma.
 272
 273 inline procedural "cic:/CoRN/reals/Series/aew_series_conv.con" as lemma.
 274
 275 (* UNEXPORTED
 276 End Almost_Everywhere
 277 *)
 278
 279 (* UNEXPORTED
 280 Section Cauchy_Almost_Everywhere
 281 *)
 282
 283 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
 284
 285 (* UNEXPORTED
 286 cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var
 287 *)
 288
 289 (* UNEXPORTED
 290 cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var
 291 *)
 292
 293 (* UNEXPORTED
 294 cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var
 295 *)
 296
 297 inline procedural "cic:/CoRN/reals/Series/aew_Lim.con" as lemma.
 298
 299 (* UNEXPORTED
 300 End Cauchy_Almost_Everywhere
 301 *)
 302
 303 (* UNEXPORTED
 304 Section Convergence_Criteria
 305 *)
 306
 307 (*#* **Convergence Criteria
 308
 309 %\begin{convention}% Let [x:nat->IR].
 310 %\end{convention}%
 311 *)
 312
 313 (* UNEXPORTED
 314 cic:/CoRN/reals/Series/Convergence_Criteria/x.var
 315 *)
 316
 317 (*#* We include the comparison test for series, both in a strong and in a less
 318 general (but simpler) form.
 319 *)
 320
 321 inline procedural "cic:/CoRN/reals/Series/str_comparison.con" as lemma.
 322
 323 inline procedural "cic:/CoRN/reals/Series/comparison.con" as lemma.
 324
 325 (*#* As a corollary, we get that every absolutely convergent series converges. *)
 326
 327 inline procedural "cic:/CoRN/reals/Series/abs_imp_conv.con" as lemma.
 328
 329 (*#* Next we have the ratio test, both as a positive and negative result. *)
 330
 331 inline procedural "cic:/CoRN/reals/Series/divergent_crit.con" as lemma.
 332
 333 inline procedural "cic:/CoRN/reals/Series/tail_series.con" as lemma.
 334
 335 inline procedural "cic:/CoRN/reals/Series/join_series.con" as lemma.
 336
 337 (* UNEXPORTED
 338 End Convergence_Criteria
 339 *)
 340
 341 (* UNEXPORTED
 342 Section More_CC
 343 *)
 344
 345 (* UNEXPORTED
 346 cic:/CoRN/reals/Series/More_CC/x.var
 347 *)
 348
 349 inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con" as lemma.
 350
 351 inline procedural "cic:/CoRN/reals/Series/ratio_test_div.con" as lemma.
 352
 353 (* UNEXPORTED
 354 End More_CC
 355 *)
 356
 357 (* UNEXPORTED
 358 Section Alternate_Series
 359 *)
 360
 361 (*#* **Alternate Series
 362
 363 Alternate series are a special case.  Suppose that [x] is nonnegative and
 364 decreasing convergent to 0.
 365 *)
 366
 367 (* UNEXPORTED
 368 cic:/CoRN/reals/Series/Alternate_Series/x.var
 369 *)
 370
 371 (* UNEXPORTED
 372 cic:/CoRN/reals/Series/Alternate_Series/pos_x.var
 373 *)
 374
 375 (* UNEXPORTED
 376 cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var
 377 *)
 378
 379 (* UNEXPORTED
 380 cic:/CoRN/reals/Series/Alternate_Series/mon_x.var
 381 *)
 382
 383 (* begin hide *)
 384
 385 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/y.con" "Alternate_Series__" as definition.
 386
 387 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma1.con" "Alternate_Series__" as definition.
 388
 389 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma2.con" "Alternate_Series__" as definition.
 390
 391 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma3.con" "Alternate_Series__" as definition.
 392
 393 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma4.con" "Alternate_Series__" as definition.
 394
 395 (* end hide *)
 396
 397 inline procedural "cic:/CoRN/reals/Series/alternate_series_conv.con" as lemma.
 398
 399 (* UNEXPORTED
 400 End Alternate_Series
 401 *)
 402
 403 (* UNEXPORTED
 404 Section Important_Numbers
 405 *)
 406
 407 (*#* **Important Numbers
 408
 409 We end this chapter by defining two important numbers in mathematics: [pi]
 410 and $e$#e#, both as sums of convergent series.
 411 *)
 412
 413 inline procedural "cic:/CoRN/reals/Series/e_series.con" as definition.
 414
 415 inline procedural "cic:/CoRN/reals/Series/e_series_conv.con" as lemma.
 416
 417 inline procedural "cic:/CoRN/reals/Series/E.con" as definition.
 418
 419 inline procedural "cic:/CoRN/reals/Series/pi_series.con" as definition.
 420
 421 inline procedural "cic:/CoRN/reals/Series/pi_series_conv.con" as lemma.
 422
 423 inline procedural "cic:/CoRN/reals/Series/pi.con" as definition.
 424
 425 (* UNEXPORTED
 426 End Important_Numbers
 427 *)
 428