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 *********************)
19 (* $Id: FTC.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
21 (*#* printing [-S-] %\ensuremath{\int}% #∫# *)
23 include "ftc/MoreIntegrals.ma".
25 include "ftc/CalculusTheorems.ma".
32 Section Indefinite_Integral
35 (*#* *The Fundamental Theorem of Calculus
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
41 **Indefinite Integrals
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.
47 %\begin{convention}% Let [I : interval], [F : PartIR] be continuous in [I]
48 and [a] be a point in [I].
52 alias id "I" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var".
54 alias id "F" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var".
56 alias id "contF" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var".
58 alias id "a" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var".
60 alias id "Ha" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var".
62 inline procedural "cic:/CoRN/ftc/FTC/prim_lemma.con" as lemma.
64 inline procedural "cic:/CoRN/ftc/FTC/Fprim_strext.con" as lemma.
66 inline procedural "cic:/CoRN/ftc/FTC/Fprim.con" as definition.
69 End Indefinite_Integral
73 Implicit Arguments Fprim [I F].
77 Notation "[-S-] F" := (Fprim F) (at level 20).
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 alias id "J" = "cic:/CoRN/ftc/FTC/FTC/J.var".
97 alias id "F" = "cic:/CoRN/ftc/FTC/FTC/F.var".
99 alias id "contF" = "cic:/CoRN/ftc/FTC/FTC/contF.var".
101 alias id "x0" = "cic:/CoRN/ftc/FTC/FTC/x0.var".
103 alias id "Hx0" = "cic:/CoRN/ftc/FTC/FTC/Hx0.var".
107 inline procedural "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__" as definition.
111 inline procedural "cic:/CoRN/ftc/FTC/Continuous_prim.con" as lemma.
114 The derivative of [G] is simply [F].
117 alias id "pJ" = "cic:/CoRN/ftc/FTC/FTC/pJ.var".
119 inline procedural "cic:/CoRN/ftc/FTC/FTC1.con" as theorem.
122 Any other function [G0] with derivative [F] must differ from [G] by a constant.
125 alias id "G0" = "cic:/CoRN/ftc/FTC/FTC/G0.var".
127 alias id "derG0" = "cic:/CoRN/ftc/FTC/FTC/derG0.var".
129 inline procedural "cic:/CoRN/ftc/FTC/FTC2.con" as theorem.
132 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
137 inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__" as definition.
145 inline procedural "cic:/CoRN/ftc/FTC/Barrow.con" as theorem.
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 alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var".
183 alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var".
185 alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var".
187 alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var".
189 alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/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 alias id "a" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var".
207 alias id "b" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var".
209 alias id "Hab" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var".
211 alias id "contIf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var".
213 alias id "contIF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var".
217 alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var".
221 alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var".
223 alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var".
225 alias id "Hx0'" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var".
229 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__" as definition.
231 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__" as definition.
237 alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var".
239 alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var".
243 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con" as lemma.
250 And now we can generalize it step by step.
253 inline procedural "cic:/CoRN/ftc/FTC/limit_of_integral.con" as lemma.
255 inline procedural "cic:/CoRN/ftc/FTC/limit_of_Integral.con" as lemma.
262 Finally, with [x0, g, G] as before,
267 alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var".
271 alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var".
273 alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var".
277 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__" as definition.
279 inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__" as definition.
283 alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var".
285 alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var".
287 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con" as lemma.
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 alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var".
310 alias id "pJ" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var".
312 alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var".
314 alias id "g" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var".
316 alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var".
318 alias id "G" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var".
320 alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var".
322 alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var".
324 alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var".
326 alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var".
328 alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var".
330 alias id "convG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var".
332 alias id "derf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var".
334 inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con" as lemma.
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 alias id "J" = "cic:/CoRN/ftc/FTC/Derivative_Series/J.var".
350 alias id "pJ" = "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var".
352 alias id "f" = "cic:/CoRN/ftc/FTC/Derivative_Series/f.var".
354 alias id "g" = "cic:/CoRN/ftc/FTC/Derivative_Series/g.var".
358 alias id "convF" = "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var".
360 alias id "convG" = "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var".
364 alias id "derF" = "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var".
366 inline procedural "cic:/CoRN/ftc/FTC/Derivative_FSeries.con" as lemma.
369 End Derivative_Series