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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/Series".
21 (* $Id: Series.v,v 1.6 2004/04/23 10:01:05 lcf Exp $ *)
23 (*#* printing seq_part_sum %\ensuremath{\sum^n}% #∑<sup>n</sup># *)
25 (*#* printing series_sum %\ensuremath{\sum_0^{\infty}}% #∑<sub>0</sub><sup>∞</sup># *)
27 (*#* printing pi %\ensuremath{\pi}% #π *)
29 include "reals/CSumsReals.ma".
31 include "reals/NRootIR.ma".
37 (*#* *Series of Real Numbers
38 In this file we develop a theory of series of real numbers.
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.
44 %\begin{convention}% Let [x:nat->IR].
48 inline "cic:/CoRN/reals/Series/x.var".
50 inline "cic:/CoRN/reals/Series/seq_part_sum.con".
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 "cic:/CoRN/reals/Series/seq_part_sum_n.con".
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 "cic:/CoRN/reals/Series/convergent.con".
66 inline "cic:/CoRN/reals/Series/series_sum.con".
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 "cic:/CoRN/reals/Series/divergent_seq.con".
76 inline "cic:/CoRN/reals/Series/divergent.con".
78 inline "cic:/CoRN/reals/Series/conv_imp_not_div.con".
80 inline "cic:/CoRN/reals/Series/div_imp_not_conv.con".
82 inline "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con".
84 inline "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con".
86 (*#* Finally we have the well known fact that every convergent series converges
87 to zero as a sequence.
90 inline "cic:/CoRN/reals/Series/series_seq_Lim.con".
92 inline "cic:/CoRN/reals/Series/series_seq_Lim'.con".
99 Section More_Definitions.
102 inline "cic:/CoRN/reals/Series/x.var".
104 (*#* We also define absolute convergence. *)
106 inline "cic:/CoRN/reals/Series/abs_convergent.con".
109 End More_Definitions.
113 Section Power_Series.
118 Power series are an important special case.
121 inline "cic:/CoRN/reals/Series/power_series.con".
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.
128 %\begin{convention}% Let [c] be a real number between 0 and 1.
132 inline "cic:/CoRN/reals/Series/c.var".
134 inline "cic:/CoRN/reals/Series/H0c.var".
136 inline "cic:/CoRN/reals/Series/Hc1.var".
138 inline "cic:/CoRN/reals/Series/c_exp_Lim.con".
140 inline "cic:/CoRN/reals/Series/power_series_Lim1.con".
142 inline "cic:/CoRN/reals/Series/power_series_conv.con".
144 inline "cic:/CoRN/reals/Series/power_series_sum.con".
156 Some operations with series preserve convergence. We start by defining
157 the series that is zero everywhere.
160 inline "cic:/CoRN/reals/Series/conv_zero_series.con".
162 inline "cic:/CoRN/reals/Series/series_sum_zero.con".
164 (*#* Next we consider extensionality, as well as the sum and difference
165 of two convergent series.
167 %\begin{convention}% Let [x,y:nat->IR] be convergent series.
171 inline "cic:/CoRN/reals/Series/x.var".
173 inline "cic:/CoRN/reals/Series/y.var".
175 inline "cic:/CoRN/reals/Series/convX.var".
177 inline "cic:/CoRN/reals/Series/convY.var".
179 inline "cic:/CoRN/reals/Series/convergent_wd.con".
181 inline "cic:/CoRN/reals/Series/series_sum_wd.con".
183 inline "cic:/CoRN/reals/Series/conv_series_plus.con".
185 inline "cic:/CoRN/reals/Series/series_sum_plus.con".
187 inline "cic:/CoRN/reals/Series/conv_series_minus.con".
189 inline "cic:/CoRN/reals/Series/series_sum_minus.con".
191 (*#* Multiplication by a scalar [c] is also permitted. *)
193 inline "cic:/CoRN/reals/Series/c.var".
195 inline "cic:/CoRN/reals/Series/conv_series_mult_scal.con".
197 inline "cic:/CoRN/reals/Series/series_sum_mult_scal.con".
204 Section More_Operations.
207 inline "cic:/CoRN/reals/Series/x.var".
209 inline "cic:/CoRN/reals/Series/convX.var".
211 (*#* As a corollary, we get the series of the inverses. *)
213 inline "cic:/CoRN/reals/Series/conv_series_inv.con".
215 inline "cic:/CoRN/reals/Series/series_sum_inv.con".
222 Section Almost_Everywhere.
225 (*#* ** Almost Everywhere
227 In this section we strengthen some of the convergence results for sequences
228 and derive an important corollary for series.
230 Let [x,y : nat->IR] be equal after some natural number.
233 inline "cic:/CoRN/reals/Series/x.var".
235 inline "cic:/CoRN/reals/Series/y.var".
237 inline "cic:/CoRN/reals/Series/aew_eq.con".
239 inline "cic:/CoRN/reals/Series/aew_equal.var".
241 inline "cic:/CoRN/reals/Series/aew_Cauchy.con".
243 inline "cic:/CoRN/reals/Series/aew_Cauchy2.con".
245 inline "cic:/CoRN/reals/Series/aew_series_conv.con".
248 End Almost_Everywhere.
252 Section Cauchy_Almost_Everywhere.
255 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
257 inline "cic:/CoRN/reals/Series/x.var".
259 inline "cic:/CoRN/reals/Series/y.var".
261 inline "cic:/CoRN/reals/Series/aew_equal.var".
263 inline "cic:/CoRN/reals/Series/aew_Lim.con".
266 End Cauchy_Almost_Everywhere.
270 Section Convergence_Criteria.
273 (*#* **Convergence Criteria
275 %\begin{convention}% Let [x:nat->IR].
279 inline "cic:/CoRN/reals/Series/x.var".
281 (*#* We include the comparison test for series, both in a strong and in a less
282 general (but simpler) form.
285 inline "cic:/CoRN/reals/Series/str_comparison.con".
287 inline "cic:/CoRN/reals/Series/comparison.con".
289 (*#* As a corollary, we get that every absolutely convergent series converges. *)
291 inline "cic:/CoRN/reals/Series/abs_imp_conv.con".
293 (*#* Next we have the ratio test, both as a positive and negative result. *)
295 inline "cic:/CoRN/reals/Series/divergent_crit.con".
297 inline "cic:/CoRN/reals/Series/tail_series.con".
299 inline "cic:/CoRN/reals/Series/join_series.con".
302 End Convergence_Criteria.
309 inline "cic:/CoRN/reals/Series/x.var".
311 inline "cic:/CoRN/reals/Series/ratio_test_conv.con".
313 inline "cic:/CoRN/reals/Series/ratio_test_div.con".
320 Section Alternate_Series.
323 (*#* **Alternate Series
325 Alternate series are a special case. Suppose that [x] is nonnegative and
326 decreasing convergent to 0.
329 inline "cic:/CoRN/reals/Series/x.var".
331 inline "cic:/CoRN/reals/Series/pos_x.var".
333 inline "cic:/CoRN/reals/Series/Lim_x.var".
335 inline "cic:/CoRN/reals/Series/mon_x.var".
339 inline "cic:/CoRN/reals/Series/y.con".
341 inline "cic:/CoRN/reals/Series/alternate_lemma1.con".
343 inline "cic:/CoRN/reals/Series/alternate_lemma2.con".
345 inline "cic:/CoRN/reals/Series/alternate_lemma3.con".
347 inline "cic:/CoRN/reals/Series/alternate_lemma4.con".
351 inline "cic:/CoRN/reals/Series/alternate_series_conv.con".
354 End Alternate_Series.
358 Section Important_Numbers.
361 (*#* **Important Numbers
363 We end this chapter by defining two important numbers in mathematics: [pi]
364 and $e$#e#, both as sums of convergent series.
367 inline "cic:/CoRN/reals/Series/e_series.con".
369 inline "cic:/CoRN/reals/Series/e_series_conv.con".
371 inline "cic:/CoRN/reals/Series/E.con".
373 inline "cic:/CoRN/reals/Series/pi_series.con".
375 inline "cic:/CoRN/reals/Series/pi_series_conv.con".
377 inline "cic:/CoRN/reals/Series/pi.con".
380 End Important_Numbers.