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

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 (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : ∀ x ∈ Set.Ioo (a ⊓ b) (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 (a ⊓ b) (a ⊔ b), HasDerivAt u (u' x) x) (hvv' : ∀ x ∈ Set.Ioo (a ⊓ b) (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 (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) (hvv' : ∀ x ∈ Set.Ioo (a ⊓ b) (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 (a ⊓ b) (a ⊔ b), HasDerivAt u (u' x) x) (hvv' : ∀ x ∈ Set.Ioo (a ⊓ b) (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 (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hg_cont : ContinuousOn g (f '' Set.Ioo (a ⊓ b) (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.

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 (a ⊓ b) (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.

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

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.

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 (a ⊓ b) (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 (f a ⊓ f b) (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 (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hg_cont : ContinuousOn g (f '' Set.Ioo (a ⊓ b) (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 (a ⊓ b) (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 (a ⊓ b) (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 (f a ⊓ f b) (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