Integration by substitution
Here we prove integration by substition. Simply put, this lemma shows that int((FoG)*G', a .. b) = int(F, G(a) .. G(b)), assuming that G is differentiable on [c, d] and that F is continuous on [c0, d0] and that G maps compact intervals into [c0, d0].Lemma IntegrationBySubstition :
forall a b
(Hab: Min a b[<=]Max a b)
c d (Hcd: c[<]d)
(Habcd: ⊆ (Compact Hab) (Compact (less_leEq _ _ _ Hcd)))
G (HGa: Dom G a) (HGb: Dom G b)
G' (HGG': Derivative_I Hcd G G')
(HGaGb: Min (G a HGa) (G b HGb)[<=]Max (G a HGa) (G b HGb))
F
c0 d0 (Hc0d0: c0[<=]d0)
(HGF: maps_into_compacts G F _ _ Hab _ _ Hc0d0)
(HFG: Continuous_I Hab ((F[o]G){*}G'))
(HF: Continuous_I HGaGb F)
(HFc0d0: Continuous_I Hc0d0 F),
∫ HFG[=]∫ HF.
Included.
Qed.
This lemma is a special instance of substituion that ties
integration on [0, 1] with general integration on [a, b].
It says that int(F((b-a)*x+a), x=0 .. 1) = int(F, a .. b).
Lemma IntegrationSubs01 : forall a b
(Hab: Min a b[<=]Max a b)
(H01: 0[<=]1)
F
(HFG: Continuous_I H01 ((F[o]([-C-](b[-]a){*}(Fid IR){+}[-C-]a))))
(HF: Continuous_I Hab F),
(b[-]a)[*]∫I _ _ _ _ HFG[=]∫ HF.