Documentation

Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Integration by parts and by substitution #

We derive additional integration techniques from FTC-2:

Versions of the change of variables formula for monotone and antitone functions, but with much weaker assumptions on the integrands and not restricted to intervals, can be found in Mathlib/MeasureTheory/Function/JacobianOneDim.lean

Tags #

integration by parts, change of variables in integrals

source
theorem intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

The integral of the derivative of a product of two maps. For improper integrals, see MeasureTheory.integral_deriv_mul_eq_sub, MeasureTheory.integral_Ioi_deriv_mul_eq_sub, and MeasureTheory.integral_Iic_deriv_mul_eq_sub.

source
theorem intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivAt {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

The integral of the derivative of a product of two maps. Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a two-sided derivative in the interior of the interval.

source
theorem intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivWithinAt {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

The integral of the derivative of a product of two maps. Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a one-sided derivative at the endpoints.

source
theorem intervalIntegral.integral_deriv_mul_eq_sub {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a derivative at the endpoints.

source
theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Integration by parts. For improper integrals, see MeasureTheory.integral_mul_deriv_eq_deriv_mul, MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul, and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.

source
theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Integration by parts. Special case of integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a two-sided derivative in the interior of the interval.

source
theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Integration by parts. Special case of intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a one-sided derivative at the endpoints.

source
theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul {a b : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A} (hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Integration by parts. Special case of intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right where the functions have a derivative also at the endpoints. For improper integrals, see MeasureTheory.integral_mul_deriv_eq_deriv_mul, MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul, and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.

source
theorem intervalIntegral.integral_deriv_smul_eq_sub_of_hasDeriv_right {a b : ℝ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [CompleteSpace E] [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u' x • v x + u x • v' x = u b • v b - u a • v a

The integral of the derivative of a scalar multiplication.

source
theorem intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right {a b : ℝ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [CompleteSpace E] [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Integration by parts (vector-valued).

source
theorem intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt {a b : ℝ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [CompleteSpace E] [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E} (hu : ContinuousOn u (Set.uIcc a b)) (hv : ContinuousOn v (Set.uIcc a b)) (huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) (hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Integration by parts (vector-valued). Special case of integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right where the functions have a two-sided derivative in the interior of the interval.

source
theorem intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivWithinAt {a b : ℝ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [CompleteSpace E] [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E} (hu : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Integration by parts (vector-valued). Special case of intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right where the functions have a one-sided derivative at the endpoints.

source
theorem intervalIntegral.integral_smul_deriv_eq_deriv_smul {a b : ℝ} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] [CompleteSpace E] [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E} (hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' MeasureTheory.volume a b) (hv' : IntervalIntegrable v' MeasureTheory.volume a b) :
∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x

Integration by parts (vector-valued). Special case of intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right where the functions have a derivative also at the endpoints.

Integration by substitution / Change of variables #

source
theorem intervalIntegral.integral_comp_smul_deriv''' {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hg_cont : ContinuousOn g (f '' Set.Ioo (min a b) (max a b))) (hg1 : MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : ℝ) => f' x • (g ∘ f) x) (Set.uIcc a b) MeasureTheory.volume) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Change of variables, general form. If f is continuous on [a, b] and has right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on f '' [a, b], and f' x • (g ∘ f) x is integrable on [a, b], then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

If the function f is monotone or antitone, see also integral_image_eq_integral_deriv_smul_of_monotoneOn dropping all assumptions on g.

source
theorem intervalIntegral.integral_comp_smul_deriv'' {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (f '' Set.uIcc a b)) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Change of variables for continuous integrands. If f is continuous on [a, b] and has continuous right-derivative f' in (a, b), and g is continuous on f '' [a, b] then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

If the function f is monotone or antitone, see also integral_image_eq_integral_deriv_smul_of_monotoneOn dropping all assumptions on g.

source
theorem intervalIntegral.integral_comp_smul_deriv' {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} (h : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (f '' Set.uIcc a b)) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x

Change of variables. If f has continuous derivative f' on [a, b], and g is continuous on f '' [a, b], then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u. Compared to intervalIntegral.integral_comp_smul_deriv we only require that g is continuous on f '' [a, b].

If the function f is monotone or antitone, see also integral_image_eq_integral_deriv_smul_of_monotoneOn dropping all assumptions on g.

source
theorem intervalIntegral.integral_comp_smul_deriv {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} (h : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (Set.uIcc a b)) (hg : Continuous g) :
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x

Change of variables, most common version. If f has continuous derivative f' on [a, b], and g is continuous, then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.

If the function f is monotone or antitone, see also integral_image_eq_integral_deriv_smul_of_monotoneOn dropping all assumptions on g.

source
theorem intervalIntegral.integral_deriv_comp_smul_deriv' {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E} [CompleteSpace E] (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (Set.uIcc (f a) (f b))) (hgg' : ∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) (hg' : ContinuousOn g' (f '' Set.uIcc a b)) :
∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
source
theorem intervalIntegral.integral_deriv_comp_smul_deriv {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E} [CompleteSpace E] (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hg : ∀ x ∈ Set.uIcc a b, HasDerivAt g (g' (f x)) (f x)) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg' : Continuous g') :
∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
source
theorem intervalIntegral.integral_comp_mul_deriv''' {a b : ℝ} {f f' g : ℝ → ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hg_cont : ContinuousOn g (f '' Set.Ioo (min a b) (max a b))) (hg1 : MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (x : ℝ) => (g ∘ f) x * f' x) (Set.uIcc a b) MeasureTheory.volume) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Change of variables, general form for scalar functions. If f is continuous on [a, b] and has continuous right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on f '' [a, b], and (g ∘ f) x * f' x is integrable on [a, b], then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

source
theorem intervalIntegral.integral_comp_mul_deriv'' {a b : ℝ} {f f' g : ℝ → ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (f '' Set.uIcc a b)) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Change of variables for continuous integrands. If f is continuous on [a, b] and has continuous right-derivative f' in (a, b), and g is continuous on f '' [a, b] then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

source
theorem intervalIntegral.integral_comp_mul_deriv' {a b : ℝ} {f f' g : ℝ → ℝ} (h : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (f '' Set.uIcc a b)) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x

Change of variables. If f has continuous derivative f' on [a, b], and g is continuous on f '' [a, b], then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u. Compared to intervalIntegral.integral_comp_mul_deriv we only require that g is continuous on f '' [a, b].

source
theorem intervalIntegral.integral_comp_mul_deriv {a b : ℝ} {f f' g : ℝ → ℝ} (h : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (Set.uIcc a b)) (hg : Continuous g) :
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x

Change of variables, most common version. If f has continuous derivative f' on [a, b], and g is continuous, then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

source
theorem intervalIntegral.integral_deriv_comp_mul_deriv' {a b : ℝ} {f f' g g' : ℝ → ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg : ContinuousOn g (Set.uIcc (f a) (f b))) (hgg' : ∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x) (hg' : ContinuousOn g' (f '' Set.uIcc a b)) :
∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
source
theorem intervalIntegral.integral_deriv_comp_mul_deriv {a b : ℝ} {f f' g g' : ℝ → ℝ} (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hg : ∀ x ∈ Set.uIcc a b, HasDerivAt g (g' (f x)) (f x)) (hf' : ContinuousOn f' (Set.uIcc a b)) (hg' : Continuous g') :
∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a