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