Integration by parts and by substitution

We derive additional integration techniques from FTC-2:

• intervalIntegral.integral_mul_deriv_eq_deriv_mul - integration by parts
• intervalIntegral.integral_comp_mul_deriv'' - integration by substitution

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 MeasureTheory.Function.JacobianOneDim

Tags

integration by parts, change of variables in integrals

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.

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.

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.

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.

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.

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.

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.

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.

Integration by substitution / Change of variables

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.

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.

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.

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.

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

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

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.

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.

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].

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.

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

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