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].
46 alias id "x" = "cic:/CoRN/reals/Series/Definitions/x.var".
48 inline procedural "cic:/CoRN/reals/Series/seq_part_sum.con" as definition.
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.
56 inline procedural "cic:/CoRN/reals/Series/seq_part_sum_n.con" as lemma.
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.
62 inline procedural "cic:/CoRN/reals/Series/convergent.con" as definition.
64 inline procedural "cic:/CoRN/reals/Series/series_sum.con" as definition.
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.
72 inline procedural "cic:/CoRN/reals/Series/divergent_seq.con" as definition.
74 inline procedural "cic:/CoRN/reals/Series/divergent.con" as definition.
76 inline procedural "cic:/CoRN/reals/Series/conv_imp_not_div.con" as lemma.
78 inline procedural "cic:/CoRN/reals/Series/div_imp_not_conv.con" as lemma.
80 inline procedural "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con" as lemma.
82 inline procedural "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con" as lemma.
84 (*#* Finally we have the well known fact that every convergent series converges
85 to zero as a sequence.
88 inline procedural "cic:/CoRN/reals/Series/series_seq_Lim.con" as lemma.
90 inline procedural "cic:/CoRN/reals/Series/series_seq_Lim'.con" as lemma.
97 Section More_Definitions
100 alias id "x" = "cic:/CoRN/reals/Series/More_Definitions/x.var".
102 (*#* We also define absolute convergence. *)
104 inline procedural "cic:/CoRN/reals/Series/abs_convergent.con" as definition.
116 Power series are an important special case.
119 inline procedural "cic:/CoRN/reals/Series/power_series.con" as definition.
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.
126 %\begin{convention}% Let [c] be a real number between 0 and 1.
130 alias id "c" = "cic:/CoRN/reals/Series/Power_Series/c.var".
132 alias id "H0c" = "cic:/CoRN/reals/Series/Power_Series/H0c.var".
134 alias id "Hc1" = "cic:/CoRN/reals/Series/Power_Series/Hc1.var".
136 inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con" as lemma.
138 inline procedural "cic:/CoRN/reals/Series/power_series_Lim1.con" as lemma.
140 inline procedural "cic:/CoRN/reals/Series/power_series_conv.con" as lemma.
142 inline procedural "cic:/CoRN/reals/Series/power_series_sum.con" as lemma.
154 Some operations with series preserve convergence. We start by defining
155 the series that is zero everywhere.
158 inline procedural "cic:/CoRN/reals/Series/conv_zero_series.con" as lemma.
160 inline procedural "cic:/CoRN/reals/Series/series_sum_zero.con" as lemma.
162 (*#* Next we consider extensionality, as well as the sum and difference
163 of two convergent series.
165 %\begin{convention}% Let [x,y:nat->IR] be convergent series.
169 alias id "x" = "cic:/CoRN/reals/Series/Operations/x.var".
171 alias id "y" = "cic:/CoRN/reals/Series/Operations/y.var".
173 alias id "convX" = "cic:/CoRN/reals/Series/Operations/convX.var".
175 alias id "convY" = "cic:/CoRN/reals/Series/Operations/convY.var".
177 inline procedural "cic:/CoRN/reals/Series/convergent_wd.con" as lemma.
179 inline procedural "cic:/CoRN/reals/Series/series_sum_wd.con" as lemma.
181 inline procedural "cic:/CoRN/reals/Series/conv_series_plus.con" as lemma.
183 inline procedural "cic:/CoRN/reals/Series/series_sum_plus.con" as lemma.
185 inline procedural "cic:/CoRN/reals/Series/conv_series_minus.con" as lemma.
187 inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con" as lemma.
189 (*#* Multiplication by a scalar [c] is also permitted. *)
191 alias id "c" = "cic:/CoRN/reals/Series/Operations/c.var".
193 inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con" as lemma.
195 inline procedural "cic:/CoRN/reals/Series/series_sum_mult_scal.con" as lemma.
202 Section More_Operations
205 alias id "x" = "cic:/CoRN/reals/Series/More_Operations/x.var".
207 alias id "convX" = "cic:/CoRN/reals/Series/More_Operations/convX.var".
209 (*#* As a corollary, we get the series of the inverses. *)
211 inline procedural "cic:/CoRN/reals/Series/conv_series_inv.con" as lemma.
213 inline procedural "cic:/CoRN/reals/Series/series_sum_inv.con" as lemma.
220 Section Almost_Everywhere
223 (*#* ** Almost Everywhere
225 In this section we strengthen some of the convergence results for sequences
226 and derive an important corollary for series.
228 Let [x,y : nat->IR] be equal after some natural number.
231 alias id "x" = "cic:/CoRN/reals/Series/Almost_Everywhere/x.var".
233 alias id "y" = "cic:/CoRN/reals/Series/Almost_Everywhere/y.var".
235 inline procedural "cic:/CoRN/reals/Series/aew_eq.con" as definition.
237 alias id "aew_equal" = "cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var".
239 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con" as lemma.
241 inline procedural "cic:/CoRN/reals/Series/aew_Cauchy2.con" as lemma.
243 inline procedural "cic:/CoRN/reals/Series/aew_series_conv.con" as lemma.
246 End Almost_Everywhere
250 Section Cauchy_Almost_Everywhere
253 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
255 alias id "x" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var".
257 alias id "y" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var".
259 alias id "aew_equal" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var".
261 inline procedural "cic:/CoRN/reals/Series/aew_Lim.con" as lemma.
264 End Cauchy_Almost_Everywhere
268 Section Convergence_Criteria
271 (*#* **Convergence Criteria
273 %\begin{convention}% Let [x:nat->IR].
277 alias id "x" = "cic:/CoRN/reals/Series/Convergence_Criteria/x.var".
279 (*#* We include the comparison test for series, both in a strong and in a less
280 general (but simpler) form.
283 inline procedural "cic:/CoRN/reals/Series/str_comparison.con" as lemma.
285 inline procedural "cic:/CoRN/reals/Series/comparison.con" as lemma.
287 (*#* As a corollary, we get that every absolutely convergent series converges. *)
289 inline procedural "cic:/CoRN/reals/Series/abs_imp_conv.con" as lemma.
291 (*#* Next we have the ratio test, both as a positive and negative result. *)
293 inline procedural "cic:/CoRN/reals/Series/divergent_crit.con" as lemma.
295 inline procedural "cic:/CoRN/reals/Series/tail_series.con" as lemma.
297 inline procedural "cic:/CoRN/reals/Series/join_series.con" as lemma.
300 End Convergence_Criteria
307 alias id "x" = "cic:/CoRN/reals/Series/More_CC/x.var".
309 inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con" as lemma.
311 inline procedural "cic:/CoRN/reals/Series/ratio_test_div.con" as lemma.
318 Section Alternate_Series
321 (*#* **Alternate Series
323 Alternate series are a special case. Suppose that [x] is nonnegative and
324 decreasing convergent to 0.
327 alias id "x" = "cic:/CoRN/reals/Series/Alternate_Series/x.var".
329 alias id "pos_x" = "cic:/CoRN/reals/Series/Alternate_Series/pos_x.var".
331 alias id "Lim_x" = "cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var".
333 alias id "mon_x" = "cic:/CoRN/reals/Series/Alternate_Series/mon_x.var".
337 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/y.con" "Alternate_Series__" as definition.
339 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma1.con" "Alternate_Series__" as definition.
341 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma2.con" "Alternate_Series__" as definition.
343 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma3.con" "Alternate_Series__" as definition.
345 inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma4.con" "Alternate_Series__" as definition.
349 inline procedural "cic:/CoRN/reals/Series/alternate_series_conv.con" as lemma.
356 Section Important_Numbers
359 (*#* **Important Numbers
361 We end this chapter by defining two important numbers in mathematics: [pi]
362 and $e$#e#, both as sums of convergent series.
365 inline procedural "cic:/CoRN/reals/Series/e_series.con" as definition.
367 inline procedural "cic:/CoRN/reals/Series/e_series_conv.con" as lemma.
369 inline procedural "cic:/CoRN/reals/Series/E.con" as definition.
371 inline procedural "cic:/CoRN/reals/Series/pi_series.con" as definition.
373 inline procedural "cic:/CoRN/reals/Series/pi_series_conv.con" as lemma.
375 inline procedural "cic:/CoRN/reals/Series/pi.con" as definition.
378 End Important_Numbers