1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: Series.v,v 1.6 2004/04/23 10:01:05 lcf Exp $ *)
21 (*#* printing seq_part_sum %\ensuremath{\sum^n}% #∑<sup>n</sup># *)
23 (*#* printing series_sum %\ensuremath{\sum_0^{\infty}}% #∑<sub>0</sub><sup>∞</sup># *)
25 (*#* printing pi %\ensuremath{\pi}% #π *)
27 include "reals/CSumsReals.ma".
29 include "reals/NRootIR.ma".
35 (*#* *Series of Real Numbers
36 In this file we develop a theory of series of real numbers.
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.
42 %\begin{convention}% Let [x:nat->IR].
47 cic:/CoRN/reals/Series/Definitions/x.var
50 inline procedural "cic:/CoRN/reals/Series/seq_part_sum.con" as definition.
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.
58 inline procedural "cic:/CoRN/reals/Series/seq_part_sum_n.con" as lemma.
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.
64 inline procedural "cic:/CoRN/reals/Series/convergent.con" as definition.
66 inline procedural "cic:/CoRN/reals/Series/series_sum.con" as definition.
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.
74 inline procedural "cic:/CoRN/reals/Series/divergent_seq.con" as definition.
76 inline procedural "cic:/CoRN/reals/Series/divergent.con" as definition.
78 inline procedural "cic:/CoRN/reals/Series/conv_imp_not_div.con" as lemma.
80 inline procedural "cic:/CoRN/reals/Series/div_imp_not_conv.con" as lemma.
82 inline procedural "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con" as lemma.
84 inline procedural "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con" as lemma.
86 (*#* Finally we have the well known fact that every convergent series converges
87 to zero as a sequence.
90 inline procedural "cic:/CoRN/reals/Series/series_seq_Lim.con" as lemma.
92 inline procedural "cic:/CoRN/reals/Series/series_seq_Lim'.con" as lemma.
99 Section More_Definitions
103 cic:/CoRN/reals/Series/More_Definitions/x.var
106 (*#* We also define absolute convergence. *)
108 inline procedural "cic:/CoRN/reals/Series/abs_convergent.con" as definition.
120 Power series are an important special case.
123 inline procedural "cic:/CoRN/reals/Series/power_series.con" as definition.
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.
130 %\begin{convention}% Let [c] be a real number between 0 and 1.
135 cic:/CoRN/reals/Series/Power_Series/c.var
139 cic:/CoRN/reals/Series/Power_Series/H0c.var
143 cic:/CoRN/reals/Series/Power_Series/Hc1.var
146 inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con" as lemma.
148 inline procedural "cic:/CoRN/reals/Series/power_series_Lim1.con" as lemma.
150 inline procedural "cic:/CoRN/reals/Series/power_series_conv.con" as lemma.
152 inline procedural "cic:/CoRN/reals/Series/power_series_sum.con" as lemma.
164 Some operations with series preserve convergence. We start by defining
165 the series that is zero everywhere.
168 inline procedural "cic:/CoRN/reals/Series/conv_zero_series.con" as lemma.
170 inline procedural "cic:/CoRN/reals/Series/series_sum_zero.con" as lemma.
172 (*#* Next we consider extensionality, as well as the sum and difference
173 of two convergent series.
175 %\begin{convention}% Let [x,y:nat->IR] be convergent series.
180 cic:/CoRN/reals/Series/Operations/x.var
184 cic:/CoRN/reals/Series/Operations/y.var
188 cic:/CoRN/reals/Series/Operations/convX.var
192 cic:/CoRN/reals/Series/Operations/convY.var
195 inline procedural "cic:/CoRN/reals/Series/convergent_wd.con" as lemma.
197 inline procedural "cic:/CoRN/reals/Series/series_sum_wd.con" as lemma.
199 inline procedural "cic:/CoRN/reals/Series/conv_series_plus.con" as lemma.
201 inline procedural "cic:/CoRN/reals/Series/series_sum_plus.con" as lemma.
203 inline procedural "cic:/CoRN/reals/Series/conv_series_minus.con" as lemma.
205 inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con" as lemma.
207 (*#* Multiplication by a scalar [c] is also permitted. *)
210 cic:/CoRN/reals/Series/Operations/c.var
213 inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con" as lemma.
215 inline procedural "cic:/CoRN/reals/Series/series_sum_mult_scal.con" as lemma.
222 Section More_Operations
226 cic:/CoRN/reals/Series/More_Operations/x.var
230 cic:/CoRN/reals/Series/More_Operations/convX.var
233 (*#* As a corollary, we get the series of the inverses. *)
235 inline procedural "cic:/CoRN/reals/Series/conv_series_inv.con" as lemma.
237 inline procedural "cic:/CoRN/reals/Series/series_sum_inv.con" as lemma.
244 Section Almost_Everywhere
247 (*#* ** Almost Everywhere
249 In this section we strengthen some of the convergence results for sequences
250 and derive an important corollary for series.
252 Let [x,y : nat->IR] be equal after some natural number.
256 cic:/CoRN/reals/Series/Almost_Everywhere/x.var
260 cic:/CoRN/reals/Series/Almost_Everywhere/y.var
263 inline procedural "cic:/CoRN/reals/Series/aew_eq.con" as definition.
266 cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var
269 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con" as lemma.
271 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy2.con" as lemma.
273 inline procedural "cic:/CoRN/reals/Series/aew_series_conv.con" as lemma.
276 End Almost_Everywhere
280 Section Cauchy_Almost_Everywhere
283 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
286 cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var
290 cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var
294 cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var
297 inline procedural "cic:/CoRN/reals/Series/aew_Lim.con" as lemma.
300 End Cauchy_Almost_Everywhere
304 Section Convergence_Criteria
307 (*#* **Convergence Criteria
309 %\begin{convention}% Let [x:nat->IR].
314 cic:/CoRN/reals/Series/Convergence_Criteria/x.var
317 (*#* We include the comparison test for series, both in a strong and in a less
318 general (but simpler) form.
321 inline procedural "cic:/CoRN/reals/Series/str_comparison.con" as lemma.
323 inline procedural "cic:/CoRN/reals/Series/comparison.con" as lemma.
325 (*#* As a corollary, we get that every absolutely convergent series converges. *)
327 inline procedural "cic:/CoRN/reals/Series/abs_imp_conv.con" as lemma.
329 (*#* Next we have the ratio test, both as a positive and negative result. *)
331 inline procedural "cic:/CoRN/reals/Series/divergent_crit.con" as lemma.
333 inline procedural "cic:/CoRN/reals/Series/tail_series.con" as lemma.
335 inline procedural "cic:/CoRN/reals/Series/join_series.con" as lemma.
338 End Convergence_Criteria
346 cic:/CoRN/reals/Series/More_CC/x.var
349 inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con" as lemma.
351 inline procedural "cic:/CoRN/reals/Series/ratio_test_div.con" as lemma.
358 Section Alternate_Series
361 (*#* **Alternate Series
363 Alternate series are a special case. Suppose that [x] is nonnegative and
364 decreasing convergent to 0.
368 cic:/CoRN/reals/Series/Alternate_Series/x.var
372 cic:/CoRN/reals/Series/Alternate_Series/pos_x.var
376 cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var
380 cic:/CoRN/reals/Series/Alternate_Series/mon_x.var
385 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/y.con" "Alternate_Series__" as definition.
387 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma1.con" "Alternate_Series__" as definition.
389 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma2.con" "Alternate_Series__" as definition.
391 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma3.con" "Alternate_Series__" as definition.
393 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma4.con" "Alternate_Series__" as definition.
397 inline procedural "cic:/CoRN/reals/Series/alternate_series_conv.con" as lemma.
404 Section Important_Numbers
407 (*#* **Important Numbers
409 We end this chapter by defining two important numbers in mathematics: [pi]
410 and $e$#e#, both as sums of convergent series.
413 inline procedural "cic:/CoRN/reals/Series/e_series.con" as definition.
415 inline procedural "cic:/CoRN/reals/Series/e_series_conv.con" as lemma.
417 inline procedural "cic:/CoRN/reals/Series/E.con" as definition.
419 inline procedural "cic:/CoRN/reals/Series/pi_series.con" as definition.
421 inline procedural "cic:/CoRN/reals/Series/pi_series_conv.con" as lemma.
423 inline procedural "cic:/CoRN/reals/Series/pi.con" as definition.
426 End Important_Numbers