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].
84 We can now prove our main theorem. We begin by remarking that the
85 primitive function is always continuous.
87 %\begin{convention}% Assume that [J : interval], [F : PartIR] is
88 continuous in [J] and [x0] is a point in [J]. Denote by [G] the
89 indefinite integral of [F] from [x0].
93 inline "cic:/CoRN/ftc/FTC/J.var".
95 inline "cic:/CoRN/ftc/FTC/F.var".
97 inline "cic:/CoRN/ftc/FTC/contF.var".
99 inline "cic:/CoRN/ftc/FTC/x0.var".
101 inline "cic:/CoRN/ftc/FTC/Hx0.var".
105 inline "cic:/CoRN/ftc/FTC/G.con".
109 inline "cic:/CoRN/ftc/FTC/Continuous_prim.con".
112 The derivative of [G] is simply [F].
115 inline "cic:/CoRN/ftc/FTC/pJ.var".
117 inline "cic:/CoRN/ftc/FTC/FTC1.con".
120 Any other function [G0] with derivative [F] must differ from [G] by a constant.
123 inline "cic:/CoRN/ftc/FTC/G0.var".
125 inline "cic:/CoRN/ftc/FTC/derG0.var".
127 inline "cic:/CoRN/ftc/FTC/FTC2.con".
130 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
135 inline "cic:/CoRN/ftc/FTC/G0_inc.con".
143 inline "cic:/CoRN/ftc/FTC/Barrow.con".
152 Hint Resolve Continuous_prim: continuous.
156 Hint Resolve FTC1: derivate.
160 Section Limit_of_Integral_Seq.
165 With these tools in our hand, we can prove several useful results.
167 %\begin{convention}% From this point onwards:
169 - [f : nat->PartIR] is a sequence of continuous functions (in [J]);
170 - [F : PartIR] is continuous in [J].
174 In the first place, if a sequence of continuous functions converges
175 then the sequence of their primitives also converges, and the limit
176 commutes with the indefinite integral.
179 inline "cic:/CoRN/ftc/FTC/J.var".
181 inline "cic:/CoRN/ftc/FTC/f.var".
183 inline "cic:/CoRN/ftc/FTC/F.var".
185 inline "cic:/CoRN/ftc/FTC/contf.var".
187 inline "cic:/CoRN/ftc/FTC/contF.var".
194 We need to prove this result first for compact intervals.
196 %\begin{convention}% Assume that [a, b, x0 : IR] with [(f n)] and [F]
197 continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by
198 [(g n)] and [G] the indefinite integrals respectively of [(f n)] and
199 [F] with origin [x0].
203 inline "cic:/CoRN/ftc/FTC/a.var".
205 inline "cic:/CoRN/ftc/FTC/b.var".
207 inline "cic:/CoRN/ftc/FTC/Hab.var".
209 inline "cic:/CoRN/ftc/FTC/contIf.var".
211 inline "cic:/CoRN/ftc/FTC/contIF.var".
215 inline "cic:/CoRN/ftc/FTC/convF.var".
219 inline "cic:/CoRN/ftc/FTC/x0.var".
221 inline "cic:/CoRN/ftc/FTC/Hx0.var".
223 inline "cic:/CoRN/ftc/FTC/Hx0'.var".
227 inline "cic:/CoRN/ftc/FTC/g.con".
229 inline "cic:/CoRN/ftc/FTC/G.con".
235 inline "cic:/CoRN/ftc/FTC/contg.var".
237 inline "cic:/CoRN/ftc/FTC/contG.var".
241 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con".
248 And now we can generalize it step by step.
251 inline "cic:/CoRN/ftc/FTC/limit_of_integral.con".
253 inline "cic:/CoRN/ftc/FTC/limit_of_Integral.con".
260 Finally, with [x0, g, G] as before,
265 inline "cic:/CoRN/ftc/FTC/convF.var".
269 inline "cic:/CoRN/ftc/FTC/x0.var".
271 inline "cic:/CoRN/ftc/FTC/Hx0.var".
275 inline "cic:/CoRN/ftc/FTC/g.con".
277 inline "cic:/CoRN/ftc/FTC/G.con".
281 inline "cic:/CoRN/ftc/FTC/contg.var".
283 inline "cic:/CoRN/ftc/FTC/contG.var".
285 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con".
292 End Limit_of_Integral_Seq.
296 Section Limit_of_Derivative_Seq.
300 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.
302 %\begin{convention}% Let [g] be the sequence of derivatives of [f] and [G] be the derivative of [F].
306 inline "cic:/CoRN/ftc/FTC/J.var".
308 inline "cic:/CoRN/ftc/FTC/pJ.var".
310 inline "cic:/CoRN/ftc/FTC/f.var".
312 inline "cic:/CoRN/ftc/FTC/g.var".
314 inline "cic:/CoRN/ftc/FTC/F.var".
316 inline "cic:/CoRN/ftc/FTC/G.var".
318 inline "cic:/CoRN/ftc/FTC/contf.var".
320 inline "cic:/CoRN/ftc/FTC/contF.var".
322 inline "cic:/CoRN/ftc/FTC/convF.var".
324 inline "cic:/CoRN/ftc/FTC/contg.var".
326 inline "cic:/CoRN/ftc/FTC/contG.var".
328 inline "cic:/CoRN/ftc/FTC/convG.var".
330 inline "cic:/CoRN/ftc/FTC/derf.var".
332 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con".
335 End Limit_of_Derivative_Seq.
339 Section Derivative_Series.
343 As a very important case of this result, we get a rule for deriving series.
346 inline "cic:/CoRN/ftc/FTC/J.var".
348 inline "cic:/CoRN/ftc/FTC/pJ.var".
350 inline "cic:/CoRN/ftc/FTC/f.var".
352 inline "cic:/CoRN/ftc/FTC/g.var".
356 inline "cic:/CoRN/ftc/FTC/convF.var".
358 inline "cic:/CoRN/ftc/FTC/convG.var".
362 inline "cic:/CoRN/ftc/FTC/derF.var".
364 inline "cic:/CoRN/ftc/FTC/Derivative_FSeries.con".
367 End Derivative_Series.