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".
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}% #π *)
39 (*#* *Series of Real Numbers
40 In this file we develop a theory of series of real numbers.
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.
46 %\begin{convention}% Let [x:nat->IR].
50 inline cic:/CoRN/reals/Series/x.var.
52 inline cic:/CoRN/reals/Series/seq_part_sum.con.
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.
60 inline cic:/CoRN/reals/Series/seq_part_sum_n.con.
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.
66 inline cic:/CoRN/reals/Series/convergent.con.
68 inline cic:/CoRN/reals/Series/series_sum.con.
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.
76 inline cic:/CoRN/reals/Series/divergent_seq.con.
78 inline cic:/CoRN/reals/Series/divergent.con.
80 inline cic:/CoRN/reals/Series/conv_imp_not_div.con.
82 inline cic:/CoRN/reals/Series/div_imp_not_conv.con.
84 inline cic:/CoRN/reals/Series/convergent_imp_not_divergent.con.
86 inline cic:/CoRN/reals/Series/divergent_imp_not_convergent.con.
88 (*#* Finally we have the well known fact that every convergent series converges
89 to zero as a sequence.
92 inline cic:/CoRN/reals/Series/series_seq_Lim.con.
94 inline cic:/CoRN/reals/Series/series_seq_Lim'.con.
101 Section More_Definitions.
104 inline cic:/CoRN/reals/Series/x.var.
106 (*#* We also define absolute convergence. *)
108 inline cic:/CoRN/reals/Series/abs_convergent.con.
111 End More_Definitions.
115 Section Power_Series.
120 Power series are an important special case.
123 inline cic:/CoRN/reals/Series/power_series.con.
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.
134 inline cic:/CoRN/reals/Series/c.var.
136 inline cic:/CoRN/reals/Series/H0c.var.
138 inline cic:/CoRN/reals/Series/Hc1.var.
140 inline cic:/CoRN/reals/Series/c_exp_Lim.con.
142 inline cic:/CoRN/reals/Series/power_series_Lim1.con.
144 inline cic:/CoRN/reals/Series/power_series_conv.con.
146 inline cic:/CoRN/reals/Series/power_series_sum.con.
158 Some operations with series preserve convergence. We start by defining
159 the series that is zero everywhere.
162 inline cic:/CoRN/reals/Series/conv_zero_series.con.
164 inline cic:/CoRN/reals/Series/series_sum_zero.con.
166 (*#* Next we consider extensionality, as well as the sum and difference
167 of two convergent series.
169 %\begin{convention}% Let [x,y:nat->IR] be convergent series.
173 inline cic:/CoRN/reals/Series/x.var.
175 inline cic:/CoRN/reals/Series/y.var.
177 inline cic:/CoRN/reals/Series/convX.var.
179 inline cic:/CoRN/reals/Series/convY.var.
181 inline cic:/CoRN/reals/Series/convergent_wd.con.
183 inline cic:/CoRN/reals/Series/series_sum_wd.con.
185 inline cic:/CoRN/reals/Series/conv_series_plus.con.
187 inline cic:/CoRN/reals/Series/series_sum_plus.con.
189 inline cic:/CoRN/reals/Series/conv_series_minus.con.
191 inline cic:/CoRN/reals/Series/series_sum_minus.con.
193 (*#* Multiplication by a scalar [c] is also permitted. *)
195 inline cic:/CoRN/reals/Series/c.var.
197 inline cic:/CoRN/reals/Series/conv_series_mult_scal.con.
199 inline cic:/CoRN/reals/Series/series_sum_mult_scal.con.
206 Section More_Operations.
209 inline cic:/CoRN/reals/Series/x.var.
211 inline cic:/CoRN/reals/Series/convX.var.
213 (*#* As a corollary, we get the series of the inverses. *)
215 inline cic:/CoRN/reals/Series/conv_series_inv.con.
217 inline cic:/CoRN/reals/Series/series_sum_inv.con.
224 Section Almost_Everywhere.
227 (*#* ** Almost Everywhere
229 In this section we strengthen some of the convergence results for sequences
230 and derive an important corollary for series.
232 Let [x,y : nat->IR] be equal after some natural number.
235 inline cic:/CoRN/reals/Series/x.var.
237 inline cic:/CoRN/reals/Series/y.var.
239 inline cic:/CoRN/reals/Series/aew_eq.con.
241 inline cic:/CoRN/reals/Series/aew_equal.var.
243 inline cic:/CoRN/reals/Series/aew_Cauchy.con.
245 inline cic:/CoRN/reals/Series/aew_Cauchy2.con.
247 inline cic:/CoRN/reals/Series/aew_series_conv.con.
250 End Almost_Everywhere.
254 Section Cauchy_Almost_Everywhere.
257 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
259 inline cic:/CoRN/reals/Series/x.var.
261 inline cic:/CoRN/reals/Series/y.var.
263 inline cic:/CoRN/reals/Series/aew_equal.var.
265 inline cic:/CoRN/reals/Series/aew_Lim.con.
268 End Cauchy_Almost_Everywhere.
272 Section Convergence_Criteria.
275 (*#* **Convergence Criteria
277 %\begin{convention}% Let [x:nat->IR].
281 inline cic:/CoRN/reals/Series/x.var.
283 (*#* We include the comparison test for series, both in a strong and in a less
284 general (but simpler) form.
287 inline cic:/CoRN/reals/Series/str_comparison.con.
289 inline cic:/CoRN/reals/Series/comparison.con.
291 (*#* As a corollary, we get that every absolutely convergent series converges. *)
293 inline cic:/CoRN/reals/Series/abs_imp_conv.con.
295 (*#* Next we have the ratio test, both as a positive and negative result. *)
297 inline cic:/CoRN/reals/Series/divergent_crit.con.
299 inline cic:/CoRN/reals/Series/tail_series.con.
301 inline cic:/CoRN/reals/Series/join_series.con.
304 End Convergence_Criteria.
311 inline cic:/CoRN/reals/Series/x.var.
313 inline cic:/CoRN/reals/Series/ratio_test_conv.con.
315 inline cic:/CoRN/reals/Series/ratio_test_div.con.
322 Section Alternate_Series.
325 (*#* **Alternate Series
327 Alternate series are a special case. Suppose that [x] is nonnegative and
328 decreasing convergent to 0.
331 inline cic:/CoRN/reals/Series/x.var.
333 inline cic:/CoRN/reals/Series/pos_x.var.
335 inline cic:/CoRN/reals/Series/Lim_x.var.
337 inline cic:/CoRN/reals/Series/mon_x.var.
341 inline cic:/CoRN/reals/Series/y.con.
343 inline cic:/CoRN/reals/Series/alternate_lemma1.con.
345 inline cic:/CoRN/reals/Series/alternate_lemma2.con.
347 inline cic:/CoRN/reals/Series/alternate_lemma3.con.
349 inline cic:/CoRN/reals/Series/alternate_lemma4.con.
353 inline cic:/CoRN/reals/Series/alternate_series_conv.con.
356 End Alternate_Series.
360 Section Important_Numbers.
363 (*#* **Important Numbers
365 We end this chapter by defining two important numbers in mathematics: [pi]
366 and $e$#e#, both as sums of convergent series.
369 inline cic:/CoRN/reals/Series/e_series.con.
371 inline cic:/CoRN/reals/Series/e_series_conv.con.
373 inline cic:/CoRN/reals/Series/E.con.
375 inline cic:/CoRN/reals/Series/pi_series.con.
377 inline cic:/CoRN/reals/Series/pi_series_conv.con.
379 inline cic:/CoRN/reals/Series/pi.con.
382 End Important_Numbers.