]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/FTC.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / FTC.mma
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 include "CoRN.ma".
18
19 (* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
20
21 (*#* printing [-S-] %\ensuremath{\int}% #∫# *)
22
23 include "ftc/MoreIntegrals.ma".
24
25 include "ftc/CalculusTheorems.ma".
26
27 (* UNEXPORTED
28 Opaque Min.
29 *)
30
31 (* UNEXPORTED
32 Section Indefinite_Integral
33 *)
34
35 (*#* *The Fundamental Theorem of Calculus
36
37 Finally we can prove the fundamental theorem of calculus and its most
38 important corollaries, which are the main tools to formalize most of
39 real analysis.
40
41 **Indefinite Integrals
42
43 We define the indefinite integral of a function in a proper interval
44 in the obvious way; we just need to state a first lemma so that the
45 continuity proofs become unnecessary.
46
47 %\begin{convention}% Let [I : interval], [F : PartIR] be continuous in [I]
48 and [a] be a point in [I].
49 %\end{convention}%
50 *)
51
52 (* UNEXPORTED
53 cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var
54 *)
55
56 (* UNEXPORTED
57 cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var
58 *)
59
60 (* UNEXPORTED
61 cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var
62 *)
63
64 (* UNEXPORTED
65 cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var
66 *)
67
68 (* UNEXPORTED
69 cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var
70 *)
71
72 inline procedural "cic:/CoRN/ftc/FTC/prim_lemma.con" as lemma.
73
74 inline procedural "cic:/CoRN/ftc/FTC/Fprim_strext.con" as lemma.
75
76 inline procedural "cic:/CoRN/ftc/FTC/Fprim.con" as definition.
77
78 (* UNEXPORTED
79 End Indefinite_Integral
80 *)
81
82 (* UNEXPORTED
83 Implicit Arguments Fprim [I F].
84 *)
85
86 (* NOTATION
87 Notation "[-S-] F" := (Fprim F) (at level 20).
88 *)
89
90 (* UNEXPORTED
91 Section FTC
92 *)
93
94 (*#* **The FTC
95
96 We can now prove our main theorem.  We begin by remarking that the
97 primitive function is always continuous.
98
99 %\begin{convention}% Assume that [J : interval], [F : PartIR] is
100 continuous in [J] and [x0] is a point in [J].  Denote by [G] the
101 indefinite integral of [F] from [x0].
102 %\end{convention}%
103 *)
104
105 (* UNEXPORTED
106 cic:/CoRN/ftc/FTC/FTC/J.var
107 *)
108
109 (* UNEXPORTED
110 cic:/CoRN/ftc/FTC/FTC/F.var
111 *)
112
113 (* UNEXPORTED
114 cic:/CoRN/ftc/FTC/FTC/contF.var
115 *)
116
117 (* UNEXPORTED
118 cic:/CoRN/ftc/FTC/FTC/x0.var
119 *)
120
121 (* UNEXPORTED
122 cic:/CoRN/ftc/FTC/FTC/Hx0.var
123 *)
124
125 (* begin hide *)
126
127 inline procedural "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__" as definition.
128
129 (* end hide *)
130
131 inline procedural "cic:/CoRN/ftc/FTC/Continuous_prim.con" as lemma.
132
133 (*#*
134 The derivative of [G] is simply [F].
135 *)
136
137 (* UNEXPORTED
138 cic:/CoRN/ftc/FTC/FTC/pJ.var
139 *)
140
141 inline procedural "cic:/CoRN/ftc/FTC/FTC1.con" as theorem.
142
143 (*#*
144 Any other function [G0] with derivative [F] must differ from [G] by a constant.
145 *)
146
147 (* UNEXPORTED
148 cic:/CoRN/ftc/FTC/FTC/G0.var
149 *)
150
151 (* UNEXPORTED
152 cic:/CoRN/ftc/FTC/FTC/derG0.var
153 *)
154
155 inline procedural "cic:/CoRN/ftc/FTC/FTC2.con" as theorem.
156
157 (*#*
158 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
159 *)
160
161 (* begin hide *)
162
163 inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__" as definition.
164
165 (* end hide *)
166
167 (* UNEXPORTED
168 Opaque G.
169 *)
170
171 inline procedural "cic:/CoRN/ftc/FTC/Barrow.con" as theorem.
172
173 (* end hide *)
174
175 (* UNEXPORTED
176 End FTC
177 *)
178
179 (* UNEXPORTED
180 Hint Resolve Continuous_prim: continuous.
181 *)
182
183 (* UNEXPORTED
184 Hint Resolve FTC1: derivate.
185 *)
186
187 (* UNEXPORTED
188 Section Limit_of_Integral_Seq
189 *)
190
191 (*#* **Corollaries
192
193 With these tools in our hand, we can prove several useful results.
194
195 %\begin{convention}% From this point onwards:
196  - [J : interval];
197  - [f : nat->PartIR] is a sequence of continuous functions (in [J]);
198  - [F : PartIR] is continuous in [J].
199
200 %\end{convention}%
201
202 In the first place, if a sequence of continuous functions converges
203 then the sequence of their primitives also converges, and the limit
204 commutes with the indefinite integral.
205 *)
206
207 (* UNEXPORTED
208 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var
209 *)
210
211 (* UNEXPORTED
212 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var
213 *)
214
215 (* UNEXPORTED
216 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var
217 *)
218
219 (* UNEXPORTED
220 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var
221 *)
222
223 (* UNEXPORTED
224 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var
225 *)
226
227 (* UNEXPORTED
228 Section Compact
229 *)
230
231 (*#*
232 We need to prove this result first for compact intervals.
233
234 %\begin{convention}% Assume that [a, b, x0 : IR] with [(f n)] and [F]
235 continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by
236 [(g n)] and [G] the indefinite integrals respectively of [(f n)] and
237 [F] with origin [x0].
238 %\end{convention}%
239 *)
240
241 (* UNEXPORTED
242 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var
243 *)
244
245 (* UNEXPORTED
246 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var
247 *)
248
249 (* UNEXPORTED
250 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var
251 *)
252
253 (* UNEXPORTED
254 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var
255 *)
256
257 (* UNEXPORTED
258 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var
259 *)
260
261 (* begin show *)
262
263 (* UNEXPORTED
264 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var
265 *)
266
267 (* end show *)
268
269 (* UNEXPORTED
270 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var
271 *)
272
273 (* UNEXPORTED
274 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var
275 *)
276
277 (* UNEXPORTED
278 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var
279 *)
280
281 (* begin hide *)
282
283 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__" as definition.
284
285 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__" as definition.
286
287 (* end hide *)
288
289 (* begin show *)
290
291 (* UNEXPORTED
292 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var
293 *)
294
295 (* UNEXPORTED
296 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var
297 *)
298
299 (* end show *)
300
301 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con" as lemma.
302
303 (* UNEXPORTED
304 End Compact
305 *)
306
307 (*#*
308 And now we can generalize it step by step.
309 *)
310
311 inline procedural "cic:/CoRN/ftc/FTC/limit_of_integral.con" as lemma.
312
313 inline procedural "cic:/CoRN/ftc/FTC/limit_of_Integral.con" as lemma.
314
315 (* UNEXPORTED
316 Section General
317 *)
318
319 (*#*
320 Finally, with [x0, g, G] as before,
321 *)
322
323 (* begin show *)
324
325 (* UNEXPORTED
326 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var
327 *)
328
329 (* end show *)
330
331 (* UNEXPORTED
332 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var
333 *)
334
335 (* UNEXPORTED
336 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var
337 *)
338
339 (* begin hide *)
340
341 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__" as definition.
342
343 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__" as definition.
344
345 (* end hide *)
346
347 (* UNEXPORTED
348 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var
349 *)
350
351 (* UNEXPORTED
352 cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var
353 *)
354
355 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con" as lemma.
356
357 (* UNEXPORTED
358 End General
359 *)
360
361 (* UNEXPORTED
362 End Limit_of_Integral_Seq
363 *)
364
365 (* UNEXPORTED
366 Section Limit_of_Derivative_Seq
367 *)
368
369 (*#*
370 Similar results hold for the sequence of derivatives of a converging sequence; this time the proof is easier, as we can do it directly for any kind of interval.
371
372 %\begin{convention}% Let [g] be the sequence of derivatives of [f] and [G] be the derivative of [F].
373 %\end{convention}%
374 *)
375
376 (* UNEXPORTED
377 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var
378 *)
379
380 (* UNEXPORTED
381 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var
382 *)
383
384 (* UNEXPORTED
385 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var
386 *)
387
388 (* UNEXPORTED
389 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var
390 *)
391
392 (* UNEXPORTED
393 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var
394 *)
395
396 (* UNEXPORTED
397 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var
398 *)
399
400 (* UNEXPORTED
401 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var
402 *)
403
404 (* UNEXPORTED
405 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var
406 *)
407
408 (* UNEXPORTED
409 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var
410 *)
411
412 (* UNEXPORTED
413 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var
414 *)
415
416 (* UNEXPORTED
417 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var
418 *)
419
420 (* UNEXPORTED
421 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var
422 *)
423
424 (* UNEXPORTED
425 cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var
426 *)
427
428 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con" as lemma.
429
430 (* UNEXPORTED
431 End Limit_of_Derivative_Seq
432 *)
433
434 (* UNEXPORTED
435 Section Derivative_Series
436 *)
437
438 (*#*
439 As a very important case of this result, we get a rule for deriving series.
440 *)
441
442 (* UNEXPORTED
443 cic:/CoRN/ftc/FTC/Derivative_Series/J.var
444 *)
445
446 (* UNEXPORTED
447 cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var
448 *)
449
450 (* UNEXPORTED
451 cic:/CoRN/ftc/FTC/Derivative_Series/f.var
452 *)
453
454 (* UNEXPORTED
455 cic:/CoRN/ftc/FTC/Derivative_Series/g.var
456 *)
457
458 (* begin show *)
459
460 (* UNEXPORTED
461 cic:/CoRN/ftc/FTC/Derivative_Series/convF.var
462 *)
463
464 (* UNEXPORTED
465 cic:/CoRN/ftc/FTC/Derivative_Series/convG.var
466 *)
467
468 (* end show *)
469
470 (* UNEXPORTED
471 cic:/CoRN/ftc/FTC/Derivative_Series/derF.var
472 *)
473
474 inline procedural "cic:/CoRN/ftc/FTC/Derivative_FSeries.con" as lemma.
475
476 (* UNEXPORTED
477 End Derivative_Series
478 *)
479