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".
19 (* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
21 (*#* printing [-S-] %\ensuremath{\int}% #∫# *)
36 Section Indefinite_Integral.
39 (*#* *The Fundamental Theorem of Calculus
41 Finally we can prove the fundamental theorem of calculus and its most
42 important corollaries, which are the main tools to formalize most of
45 **Indefinite Integrals
47 We define the indefinite integral of a function in a proper interval
48 in the obvious way; we just need to state a first lemma so that the
49 continuity proofs become unnecessary.
51 %\begin{convention}% Let [I : interval], [F : PartIR] be continuous in [I]
52 and [a] be a point in [I].
56 inline cic:/CoRN/ftc/FTC/I.var.
58 inline cic:/CoRN/ftc/FTC/F.var.
60 inline cic:/CoRN/ftc/FTC/contF.var.
62 inline cic:/CoRN/ftc/FTC/a.var.
64 inline cic:/CoRN/ftc/FTC/Ha.var.
66 inline cic:/CoRN/ftc/FTC/prim_lemma.con.
68 inline cic:/CoRN/ftc/FTC/Fprim_strext.con.
70 inline cic:/CoRN/ftc/FTC/Fprim.con.
73 End Indefinite_Integral.
77 Implicit Arguments Fprim [I F].
86 We can now prove our main theorem. We begin by remarking that the
87 primitive function is always continuous.
89 %\begin{convention}% Assume that [J : interval], [F : PartIR] is
90 continuous in [J] and [x0] is a point in [J]. Denote by [G] the
91 indefinite integral of [F] from [x0].
95 inline cic:/CoRN/ftc/FTC/J.var.
97 inline cic:/CoRN/ftc/FTC/F.var.
99 inline cic:/CoRN/ftc/FTC/contF.var.
101 inline cic:/CoRN/ftc/FTC/x0.var.
103 inline cic:/CoRN/ftc/FTC/Hx0.var.
107 inline cic:/CoRN/ftc/FTC/G.con.
111 inline cic:/CoRN/ftc/FTC/Continuous_prim.con.
114 The derivative of [G] is simply [F].
117 inline cic:/CoRN/ftc/FTC/pJ.var.
119 inline cic:/CoRN/ftc/FTC/FTC1.con.
122 Any other function [G0] with derivative [F] must differ from [G] by a constant.
125 inline cic:/CoRN/ftc/FTC/G0.var.
127 inline cic:/CoRN/ftc/FTC/derG0.var.
129 inline cic:/CoRN/ftc/FTC/FTC2.con.
132 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
137 inline cic:/CoRN/ftc/FTC/G0_inc.con.
145 inline cic:/CoRN/ftc/FTC/Barrow.con.
154 Hint Resolve Continuous_prim: continuous.
158 Hint Resolve FTC1: derivate.
162 Section Limit_of_Integral_Seq.
167 With these tools in our hand, we can prove several useful results.
169 %\begin{convention}% From this point onwards:
171 - [f : nat->PartIR] is a sequence of continuous functions (in [J]);
172 - [F : PartIR] is continuous in [J].
176 In the first place, if a sequence of continuous functions converges
177 then the sequence of their primitives also converges, and the limit
178 commutes with the indefinite integral.
181 inline cic:/CoRN/ftc/FTC/J.var.
183 inline cic:/CoRN/ftc/FTC/f.var.
185 inline cic:/CoRN/ftc/FTC/F.var.
187 inline cic:/CoRN/ftc/FTC/contf.var.
189 inline cic:/CoRN/ftc/FTC/contF.var.
196 We need to prove this result first for compact intervals.
198 %\begin{convention}% Assume that [a, b, x0 : IR] with [(f n)] and [F]
199 continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by
200 [(g n)] and [G] the indefinite integrals respectively of [(f n)] and
201 [F] with origin [x0].
205 inline cic:/CoRN/ftc/FTC/a.var.
207 inline cic:/CoRN/ftc/FTC/b.var.
209 inline cic:/CoRN/ftc/FTC/Hab.var.
211 inline cic:/CoRN/ftc/FTC/contIf.var.
213 inline cic:/CoRN/ftc/FTC/contIF.var.
217 inline cic:/CoRN/ftc/FTC/convF.var.
221 inline cic:/CoRN/ftc/FTC/x0.var.
223 inline cic:/CoRN/ftc/FTC/Hx0.var.
225 inline cic:/CoRN/ftc/FTC/Hx0'.var.
229 inline cic:/CoRN/ftc/FTC/g.con.
231 inline cic:/CoRN/ftc/FTC/G.con.
237 inline cic:/CoRN/ftc/FTC/contg.var.
239 inline cic:/CoRN/ftc/FTC/contG.var.
243 inline cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con.
250 And now we can generalize it step by step.
253 inline cic:/CoRN/ftc/FTC/limit_of_integral.con.
255 inline cic:/CoRN/ftc/FTC/limit_of_Integral.con.
262 Finally, with [x0, g, G] as before,
267 inline cic:/CoRN/ftc/FTC/convF.var.
271 inline cic:/CoRN/ftc/FTC/x0.var.
273 inline cic:/CoRN/ftc/FTC/Hx0.var.
277 inline cic:/CoRN/ftc/FTC/g.con.
279 inline cic:/CoRN/ftc/FTC/G.con.
283 inline cic:/CoRN/ftc/FTC/contg.var.
285 inline cic:/CoRN/ftc/FTC/contG.var.
287 inline cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con.
294 End Limit_of_Integral_Seq.
298 Section Limit_of_Derivative_Seq.
302 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.
304 %\begin{convention}% Let [g] be the sequence of derivatives of [f] and [G] be the derivative of [F].
308 inline cic:/CoRN/ftc/FTC/J.var.
310 inline cic:/CoRN/ftc/FTC/pJ.var.
312 inline cic:/CoRN/ftc/FTC/f.var.
314 inline cic:/CoRN/ftc/FTC/g.var.
316 inline cic:/CoRN/ftc/FTC/F.var.
318 inline cic:/CoRN/ftc/FTC/G.var.
320 inline cic:/CoRN/ftc/FTC/contf.var.
322 inline cic:/CoRN/ftc/FTC/contF.var.
324 inline cic:/CoRN/ftc/FTC/convF.var.
326 inline cic:/CoRN/ftc/FTC/contg.var.
328 inline cic:/CoRN/ftc/FTC/contG.var.
330 inline cic:/CoRN/ftc/FTC/convG.var.
332 inline cic:/CoRN/ftc/FTC/derf.var.
334 inline cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con.
337 End Limit_of_Derivative_Seq.
341 Section Derivative_Series.
345 As a very important case of this result, we get a rule for deriving series.
348 inline cic:/CoRN/ftc/FTC/J.var.
350 inline cic:/CoRN/ftc/FTC/pJ.var.
352 inline cic:/CoRN/ftc/FTC/f.var.
354 inline cic:/CoRN/ftc/FTC/g.var.
358 inline cic:/CoRN/ftc/FTC/convF.var.
360 inline cic:/CoRN/ftc/FTC/convG.var.
364 inline cic:/CoRN/ftc/FTC/derF.var.
366 inline cic:/CoRN/ftc/FTC/Derivative_FSeries.con.
369 End Derivative_Series.