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/ftc/FTC".
21 (* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
23 (*#* printing [-S-] %\ensuremath{\int}% #∫# *)
25 include "ftc/MoreIntegrals.ma".
27 include "ftc/CalculusTheorems.ma".
34 Section Indefinite_Integral.
37 (*#* *The Fundamental Theorem of Calculus
39 Finally we can prove the fundamental theorem of calculus and its most
40 important corollaries, which are the main tools to formalize most of
43 **Indefinite Integrals
45 We define the indefinite integral of a function in a proper interval
46 in the obvious way; we just need to state a first lemma so that the
47 continuity proofs become unnecessary.
49 %\begin{convention}% Let [I : interval], [F : PartIR] be continuous in [I]
50 and [a] be a point in [I].
54 inline "cic:/CoRN/ftc/FTC/I.var".
56 inline "cic:/CoRN/ftc/FTC/F.var".
58 inline "cic:/CoRN/ftc/FTC/contF.var".
60 inline "cic:/CoRN/ftc/FTC/a.var".
62 inline "cic:/CoRN/ftc/FTC/Ha.var".
64 inline "cic:/CoRN/ftc/FTC/prim_lemma.con".
66 inline "cic:/CoRN/ftc/FTC/Fprim_strext.con".
68 inline "cic:/CoRN/ftc/FTC/Fprim.con".
71 End Indefinite_Integral.
75 Implicit Arguments Fprim [I F].
79 Notation "[-S-] F" := (Fprim F) (at level 20).
88 We can now prove our main theorem. We begin by remarking that the
89 primitive function is always continuous.
91 %\begin{convention}% Assume that [J : interval], [F : PartIR] is
92 continuous in [J] and [x0] is a point in [J]. Denote by [G] the
93 indefinite integral of [F] from [x0].
97 inline "cic:/CoRN/ftc/FTC/J.var".
99 inline "cic:/CoRN/ftc/FTC/F.var".
101 inline "cic:/CoRN/ftc/FTC/contF.var".
103 inline "cic:/CoRN/ftc/FTC/x0.var".
105 inline "cic:/CoRN/ftc/FTC/Hx0.var".
109 inline "cic:/CoRN/ftc/FTC/G.con".
113 inline "cic:/CoRN/ftc/FTC/Continuous_prim.con".
116 The derivative of [G] is simply [F].
119 inline "cic:/CoRN/ftc/FTC/pJ.var".
121 inline "cic:/CoRN/ftc/FTC/FTC1.con".
124 Any other function [G0] with derivative [F] must differ from [G] by a constant.
127 inline "cic:/CoRN/ftc/FTC/G0.var".
129 inline "cic:/CoRN/ftc/FTC/derG0.var".
131 inline "cic:/CoRN/ftc/FTC/FTC2.con".
134 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
139 inline "cic:/CoRN/ftc/FTC/G0_inc.con".
147 inline "cic:/CoRN/ftc/FTC/Barrow.con".
156 Hint Resolve Continuous_prim: continuous.
160 Hint Resolve FTC1: derivate.
164 Section Limit_of_Integral_Seq.
169 With these tools in our hand, we can prove several useful results.
171 %\begin{convention}% From this point onwards:
173 - [f : nat->PartIR] is a sequence of continuous functions (in [J]);
174 - [F : PartIR] is continuous in [J].
178 In the first place, if a sequence of continuous functions converges
179 then the sequence of their primitives also converges, and the limit
180 commutes with the indefinite integral.
183 inline "cic:/CoRN/ftc/FTC/J.var".
185 inline "cic:/CoRN/ftc/FTC/f.var".
187 inline "cic:/CoRN/ftc/FTC/F.var".
189 inline "cic:/CoRN/ftc/FTC/contf.var".
191 inline "cic:/CoRN/ftc/FTC/contF.var".
198 We need to prove this result first for compact intervals.
200 %\begin{convention}% Assume that [a, b, x0 : IR] with [(f n)] and [F]
201 continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by
202 [(g n)] and [G] the indefinite integrals respectively of [(f n)] and
203 [F] with origin [x0].
207 inline "cic:/CoRN/ftc/FTC/a.var".
209 inline "cic:/CoRN/ftc/FTC/b.var".
211 inline "cic:/CoRN/ftc/FTC/Hab.var".
213 inline "cic:/CoRN/ftc/FTC/contIf.var".
215 inline "cic:/CoRN/ftc/FTC/contIF.var".
219 inline "cic:/CoRN/ftc/FTC/convF.var".
223 inline "cic:/CoRN/ftc/FTC/x0.var".
225 inline "cic:/CoRN/ftc/FTC/Hx0.var".
227 inline "cic:/CoRN/ftc/FTC/Hx0'.var".
231 inline "cic:/CoRN/ftc/FTC/g.con".
233 inline "cic:/CoRN/ftc/FTC/G.con".
239 inline "cic:/CoRN/ftc/FTC/contg.var".
241 inline "cic:/CoRN/ftc/FTC/contG.var".
245 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con".
252 And now we can generalize it step by step.
255 inline "cic:/CoRN/ftc/FTC/limit_of_integral.con".
257 inline "cic:/CoRN/ftc/FTC/limit_of_Integral.con".
264 Finally, with [x0, g, G] as before,
269 inline "cic:/CoRN/ftc/FTC/convF.var".
273 inline "cic:/CoRN/ftc/FTC/x0.var".
275 inline "cic:/CoRN/ftc/FTC/Hx0.var".
279 inline "cic:/CoRN/ftc/FTC/g.con".
281 inline "cic:/CoRN/ftc/FTC/G.con".
285 inline "cic:/CoRN/ftc/FTC/contg.var".
287 inline "cic:/CoRN/ftc/FTC/contG.var".
289 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con".
296 End Limit_of_Integral_Seq.
300 Section Limit_of_Derivative_Seq.
304 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.
306 %\begin{convention}% Let [g] be the sequence of derivatives of [f] and [G] be the derivative of [F].
310 inline "cic:/CoRN/ftc/FTC/J.var".
312 inline "cic:/CoRN/ftc/FTC/pJ.var".
314 inline "cic:/CoRN/ftc/FTC/f.var".
316 inline "cic:/CoRN/ftc/FTC/g.var".
318 inline "cic:/CoRN/ftc/FTC/F.var".
320 inline "cic:/CoRN/ftc/FTC/G.var".
322 inline "cic:/CoRN/ftc/FTC/contf.var".
324 inline "cic:/CoRN/ftc/FTC/contF.var".
326 inline "cic:/CoRN/ftc/FTC/convF.var".
328 inline "cic:/CoRN/ftc/FTC/contg.var".
330 inline "cic:/CoRN/ftc/FTC/contG.var".
332 inline "cic:/CoRN/ftc/FTC/convG.var".
334 inline "cic:/CoRN/ftc/FTC/derf.var".
336 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con".
339 End Limit_of_Derivative_Seq.
343 Section Derivative_Series.
347 As a very important case of this result, we get a rule for deriving series.
350 inline "cic:/CoRN/ftc/FTC/J.var".
352 inline "cic:/CoRN/ftc/FTC/pJ.var".
354 inline "cic:/CoRN/ftc/FTC/f.var".
356 inline "cic:/CoRN/ftc/FTC/g.var".
360 inline "cic:/CoRN/ftc/FTC/convF.var".
362 inline "cic:/CoRN/ftc/FTC/convG.var".
366 inline "cic:/CoRN/ftc/FTC/derF.var".
368 inline "cic:/CoRN/ftc/FTC/Derivative_FSeries.con".
371 End Derivative_Series.