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