The Fundamental Theorem of Calculus
Finally we can prove the fundamental theorem of calculus and its most important corollaries, which are the main tools to formalize most of real analysis.
Indefinite Integrals
We define the indefinite integral of a function in a proper interval in the obvious way; we just need to state a first lemma so that the continuity proofs become unnecessary.
Let I : interval, F : PartIR be continuous in I and a be a point in I.
Variable I : interval.
Variable F : PartIR.
Hypothesis contF : Continuous I F.
Variable a : IR.
Hypothesis Ha : I a.
Lemma prim_lemma : forall x : IR, I x -> Continuous_I (Min_leEq_Max a x) F.
Included.
Qed.
Lemma Fprim_strext : forall x y Hx Hy,
∫ (prim_lemma x Hx) [#] ∫ (prim_lemma y Hy) -> x [#] y.
Definition Fprim : PartIR.
Defined.
End Indefinite_Integral.
Notation "∫ F" := (Fprim F) (at level 20).
Section FTC.
The FTC
We can now prove our main theorem. We begin by remarking that the primitive function is always continuous.
Assume that J : interval, F : PartIR is continuous in J and x0 is a point in J. Denote by G the indefinite integral of F from x0.
Variable J : interval.
Variable F : PartIR.
Hypothesis contF : Continuous J F.
Variable x0 : IR.
Hypothesis Hx0 : J x0.
Lemma Continuous_prim : Continuous J G.
Included.
Included.
Included.
Included.
Qed.
The derivative of G is simply F.
Hypothesis pJ : proper J.
Theorem FTC1 : Derivative J pJ G F.
Included.
Included.
Included.
Included.
Qed.
Any other function G0 with derivative F must differ from G by a constant.
Variable G0 : PartIR.
Hypothesis derG0 : Derivative J pJ G0 F.
Theorem FTC2 : {c : IR | ≈ J (G{-}G0) [-C-]c}.
The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
End FTC.
Theorem Barrow : forall J F (contF : Continuous J F)
(pJ:proper J) G0 (derG0 : Derivative J pJ G0 F)
a b (H : Continuous_I (Min_leEq_Max a b) F) Ha Hb,
let Ha' := Derivative_imp_inc _ _ _ _ derG0 a Ha in let Hb' := Derivative_imp_inc _ _ _ _ derG0 b Hb in ∫ H [=] G0 b Hb'[-]G0 a Ha'.
Section Limit_of_Integral_Seq.
Corollaries
With these tools in our hand, we can prove several useful results.
From this point onwards:
- J : interval;
- f : N->PartIR is a sequence of continuous functions (in J);
- F : PartIR is continuous in J.
In the first place, if a sequence of continuous functions converges then the sequence of their primitives also converges, and the limit commutes with the indefinite integral.
Variable J : interval.
Variable f : N -> PartIR.
Variable F : PartIR.
Hypothesis contf : forall n : N, Continuous J (f n).
Hypothesis contF : Continuous J F.
Section Compact.
We need to prove this result first for compact intervals.
Assume that a, b, x0 : IR with (f n) and F continuous in [a,b], x0∈[a,b]; denote by (g n) and G the indefinite integrals respectively of (f n) and F with origin x0.
Assume that a, b, x0 : IR with (f n) and F continuous in [a,b], x0∈[a,b]; denote by (g n) and G the indefinite integrals respectively of (f n) and F with origin x0.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Hypothesis contIf : forall n : N, Continuous_I Hab (f n).
Hypothesis contIF : Continuous_I Hab F.
Hypothesis convF : conv_fun_seq' a b Hab f F contIf contIF.
Variable x0 : IR.
Hypothesis Hx0 : J x0.
Hypothesis Hx0' : Compact Hab x0.
Hypothesis contg : forall n : N, Continuous_I Hab (g n).
Hypothesis contG : Continuous_I Hab G.
Lemma fun_lim_seq_integral : conv_fun_seq' a b Hab g G contg contG.
End Compact.
And now we can generalize it step by step.
Lemma limit_of_integral : conv_fun_seq'_IR J f F contf contF -> forall x y Hxy,
⊆ (Compact Hxy) J -> forall Hf HF,
Cauchy_Lim_prop2 (fun n => ∫I x y Hxy (f n) (Hf n)) (∫I x y Hxy F HF).
Lemma limit_of_Integral : conv_fun_seq'_IR J f F contf contF -> forall x y,
⊆ (Compact (Min_leEq_Max x y)) J -> forall Hxy Hf HF,
Cauchy_Lim_prop2 (fun n => ∫ (a:=x) (b:=y) (Hab:=Hxy) (F:=f n) (Hf n))
(∫ (Hab:=Hxy) (F:=F) HF).
Section General.
Finally, with x0, g, G as before,
Hypothesis convF : conv_fun_seq'_IR J f F contf contF.
Variable x0 : IR.
Hypothesis Hx0 : J x0.
Hypothesis contg : forall n : N, Continuous J (g n).
Hypothesis contG : Continuous J G.
Lemma fun_lim_seq_integral_IR : conv_fun_seq'_IR J g G contg contG.
Included.
Qed.
End General.
End Limit_of_Integral_Seq.
Section Limit_of_Derivative_Seq.
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.
Let g be the sequence of derivatives of f and G be the derivative of F.
Let g be the sequence of derivatives of f and G be the derivative of F.
Variable J : interval.
Hypothesis pJ : proper J.
Variables f g : N -> PartIR.
Variables F G : PartIR.
Hypothesis contf : forall n : N, Continuous J (f n).
Hypothesis contF : Continuous J F.
Hypothesis convF : conv_fun_seq'_IR J f F contf contF.
Hypothesis contg : forall n : N, Continuous J (g n).
Hypothesis contG : Continuous J G.
Hypothesis convG : conv_fun_seq'_IR J g G contg contG.
Hypothesis derf : forall n : N, Derivative J pJ (f n) (g n).
Lemma fun_lim_seq_derivative : Derivative J pJ F G.
End Limit_of_Derivative_Seq.
Section Derivative_Series.
As a very important case of this result, we get a rule for deriving series.
Variable J : interval.
Hypothesis pJ : proper J.
Variables f g : N -> PartIR.
Hypothesis convF : fun_series_convergent_IR J f.
Hypothesis convG : fun_series_convergent_IR J g.
Hypothesis derF : forall n : N, Derivative J pJ (f n) (g n).
Lemma Derivative_FSeries : Derivative J pJ (∑'∞ convF) (∑'∞ convG).
End Derivative_Series.