Documentation

Mathlib.Analysis.SpecialFunctions.Integrals

Integration of specific interval integrals #

This file contains proofs of the integrals of various specific functions. This includes:

With these lemmas, many simple integrals can be computed by simp or norm_num. See test/integration.lean for specific examples.

This file also contains some facts about the interval integrability of specific functions.

This file is still being developed.

Tags #

integrate, integration, integrable, integrability

Interval integrability #

theorem intervalIntegral.intervalIntegrable_rpow {a : } {b : } {μ : MeasureTheory.Measure } [MeasureTheory.IsLocallyFiniteMeasure μ] {r : } (h : 0 r 0Set.uIcc a b) :
IntervalIntegrable (fun (x : ) => x ^ r) μ a b

See intervalIntegrable_rpow' for a version with a weaker hypothesis on r, but assuming the measure is volume.

theorem intervalIntegral.intervalIntegrable_rpow' {a : } {b : } {r : } (h : -1 < r) :
IntervalIntegrable (fun (x : ) => x ^ r) MeasureTheory.volume a b

See intervalIntegrable_rpow for a version applying to any locally finite measure, but with a stronger hypothesis on r.

theorem intervalIntegral.integrableOn_Ioo_rpow_iff {s : } {t : } (ht : 0 < t) :
MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) (Set.Ioo 0 t) MeasureTheory.volume -1 < s

The power function x ↦ x^s is integrable on (0, t) iff -1 < s.

theorem intervalIntegral.intervalIntegrable_cpow {a : } {b : } {μ : MeasureTheory.Measure } [MeasureTheory.IsLocallyFiniteMeasure μ] {r : } (h : 0 r.re 0Set.uIcc a b) :
IntervalIntegrable (fun (x : ) => x ^ r) μ a b

See intervalIntegrable_cpow' for a version with a weaker hypothesis on r, but assuming the measure is volume.

theorem intervalIntegral.intervalIntegrable_cpow' {a : } {b : } {r : } (h : -1 < r.re) :
IntervalIntegrable (fun (x : ) => x ^ r) MeasureTheory.volume a b

See intervalIntegrable_cpow for a version applying to any locally finite measure, but with a stronger hypothesis on r.

theorem intervalIntegral.integrableOn_Ioo_cpow_iff {s : } {t : } (ht : 0 < t) :
MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) (Set.Ioo 0 t) MeasureTheory.volume -1 < s.re

The complex power function x ↦ x^s is integrable on (0, t) iff -1 < s.re.

theorem intervalIntegral.intervalIntegrable_one_div {a : } {b : } {f : } {μ : MeasureTheory.Measure } [MeasureTheory.IsLocallyFiniteMeasure μ] (h : xSet.uIcc a b, f x 0) (hf : ContinuousOn f (Set.uIcc a b)) :
IntervalIntegrable (fun (x : ) => 1 / f x) μ a b
@[simp]
theorem intervalIntegral.intervalIntegrable_inv {a : } {b : } {f : } {μ : MeasureTheory.Measure } [MeasureTheory.IsLocallyFiniteMeasure μ] (h : xSet.uIcc a b, f x 0) (hf : ContinuousOn f (Set.uIcc a b)) :
IntervalIntegrable (fun (x : ) => (f x)⁻¹) μ a b
@[simp]
theorem IntervalIntegrable.log {a : } {b : } {f : } {μ : MeasureTheory.Measure } [MeasureTheory.IsLocallyFiniteMeasure μ] (hf : ContinuousOn f (Set.uIcc a b)) (h : xSet.uIcc a b, f x 0) :
IntervalIntegrable (fun (x : ) => Real.log (f x)) μ a b

Integrals of the form c * ∫ x in a..b, f (c * x + d) #

theorem intervalIntegral.mul_integral_comp_mul_right {a : } {b : } {f : } (c : ) :
c * ∫ (x : ) in a..b, f (x * c) = ∫ (x : ) in a * c..b * c, f x
theorem intervalIntegral.mul_integral_comp_mul_left {a : } {b : } {f : } (c : ) :
c * ∫ (x : ) in a..b, f (c * x) = ∫ (x : ) in c * a..c * b, f x
theorem intervalIntegral.inv_mul_integral_comp_div {a : } {b : } {f : } (c : ) :
c⁻¹ * ∫ (x : ) in a..b, f (x / c) = ∫ (x : ) in a / c..b / c, f x
theorem intervalIntegral.mul_integral_comp_mul_add {a : } {b : } {f : } (c : ) (d : ) :
c * ∫ (x : ) in a..b, f (c * x + d) = ∫ (x : ) in c * a + d..c * b + d, f x
theorem intervalIntegral.mul_integral_comp_add_mul {a : } {b : } {f : } (c : ) (d : ) :
c * ∫ (x : ) in a..b, f (d + c * x) = ∫ (x : ) in d + c * a..d + c * b, f x
theorem intervalIntegral.inv_mul_integral_comp_div_add {a : } {b : } {f : } (c : ) (d : ) :
c⁻¹ * ∫ (x : ) in a..b, f (x / c + d) = ∫ (x : ) in a / c + d..b / c + d, f x
theorem intervalIntegral.inv_mul_integral_comp_add_div {a : } {b : } {f : } (c : ) (d : ) :
c⁻¹ * ∫ (x : ) in a..b, f (d + x / c) = ∫ (x : ) in d + a / c..d + b / c, f x
theorem intervalIntegral.mul_integral_comp_mul_sub {a : } {b : } {f : } (c : ) (d : ) :
c * ∫ (x : ) in a..b, f (c * x - d) = ∫ (x : ) in c * a - d..c * b - d, f x
theorem intervalIntegral.mul_integral_comp_sub_mul {a : } {b : } {f : } (c : ) (d : ) :
c * ∫ (x : ) in a..b, f (d - c * x) = ∫ (x : ) in d - c * b..d - c * a, f x
theorem intervalIntegral.inv_mul_integral_comp_div_sub {a : } {b : } {f : } (c : ) (d : ) :
c⁻¹ * ∫ (x : ) in a..b, f (x / c - d) = ∫ (x : ) in a / c - d..b / c - d, f x
theorem intervalIntegral.inv_mul_integral_comp_sub_div {a : } {b : } {f : } (c : ) (d : ) :
c⁻¹ * ∫ (x : ) in a..b, f (d - x / c) = ∫ (x : ) in d - b / c..d - a / c, f x

Integrals of simple functions #

theorem integral_cpow {a : } {b : } {r : } (h : -1 < r.re r -1 0Set.uIcc a b) :
∫ (x : ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
theorem integral_rpow {a : } {b : } {r : } (h : -1 < r r -1 0Set.uIcc a b) :
∫ (x : ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
theorem integral_zpow {a : } {b : } {n : } (h : 0 n n -1 0Set.uIcc a b) :
∫ (x : ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1)
@[simp]
theorem integral_pow {a : } {b : } (n : ) :
∫ (x : ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1)
theorem integral_pow_abs_sub_uIoc {a : } {b : } (n : ) :
∫ (x : ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (n + 1)

Integral of |x - a| ^ n over Ι a b. This integral appears in the proof of the Picard-Lindelöf/Cauchy-Lipschitz theorem.

@[simp]
theorem integral_id {a : } {b : } :
∫ (x : ) in a..b, x = (b ^ 2 - a ^ 2) / 2
theorem integral_one {a : } {b : } :
∫ (x : ) in a..b, 1 = b - a
theorem integral_const_on_unit_interval {a : } {b : } :
∫ (x : ) in a..a + 1, b = b
@[simp]
theorem integral_inv {a : } {b : } (h : 0Set.uIcc a b) :
∫ (x : ) in a..b, x⁻¹ = Real.log (b / a)
@[simp]
theorem integral_inv_of_pos {a : } {b : } (ha : 0 < a) (hb : 0 < b) :
∫ (x : ) in a..b, x⁻¹ = Real.log (b / a)
@[simp]
theorem integral_inv_of_neg {a : } {b : } (ha : a < 0) (hb : b < 0) :
∫ (x : ) in a..b, x⁻¹ = Real.log (b / a)
theorem integral_one_div {a : } {b : } (h : 0Set.uIcc a b) :
∫ (x : ) in a..b, 1 / x = Real.log (b / a)
theorem integral_one_div_of_pos {a : } {b : } (ha : 0 < a) (hb : 0 < b) :
∫ (x : ) in a..b, 1 / x = Real.log (b / a)
theorem integral_one_div_of_neg {a : } {b : } (ha : a < 0) (hb : b < 0) :
∫ (x : ) in a..b, 1 / x = Real.log (b / a)
@[simp]
theorem integral_exp {a : } {b : } :
∫ (x : ) in a..b, Real.exp x = Real.exp b - Real.exp a
theorem integral_exp_mul_complex {a : } {b : } {c : } (hc : c 0) :
∫ (x : ) in a..b, Complex.exp (c * x) = (Complex.exp (c * b) - Complex.exp (c * a)) / c
@[simp]
theorem integral_log {a : } {b : } (h : 0Set.uIcc a b) :
∫ (x : ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
@[simp]
theorem integral_log_of_pos {a : } {b : } (ha : 0 < a) (hb : 0 < b) :
∫ (x : ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
@[simp]
theorem integral_log_of_neg {a : } {b : } (ha : a < 0) (hb : b < 0) :
∫ (x : ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
@[simp]
theorem integral_sin {a : } {b : } :
∫ (x : ) in a..b, Real.sin x = Real.cos a - Real.cos b
@[simp]
theorem integral_cos {a : } {b : } :
∫ (x : ) in a..b, Real.cos x = Real.sin b - Real.sin a
theorem integral_cos_mul_complex {z : } (hz : z 0) (a : ) (b : ) :
∫ (x : ) in a..b, Complex.cos (z * x) = Complex.sin (z * b) / z - Complex.sin (z * a) / z
theorem integral_cos_sq_sub_sin_sq {a : } {b : } :
∫ (x : ) in a..b, Real.cos x ^ 2 - Real.sin x ^ 2 = Real.sin b * Real.cos b - Real.sin a * Real.cos a
theorem integral_one_div_one_add_sq {a : } {b : } :
∫ (x : ) in a..b, 1 / (1 + x ^ 2) = Real.arctan b - Real.arctan a
@[simp]
theorem integral_inv_one_add_sq {a : } {b : } :
∫ (x : ) in a..b, (1 + x ^ 2)⁻¹ = Real.arctan b - Real.arctan a
theorem integral_mul_cpow_one_add_sq {a : } {b : } {t : } (ht : t -1) :
∫ (x : ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
theorem integral_mul_rpow_one_add_sq {a : } {b : } {t : } (ht : t -1) :
∫ (x : ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))

Integral of sin x ^ n #

theorem integral_sin_pow_aux {a : } {b : } (n : ) :
∫ (x : ) in a..b, Real.sin x ^ (n + 2) = (Real.sin a ^ (n + 1) * Real.cos a - Real.sin b ^ (n + 1) * Real.cos b + (n + 1) * ∫ (x : ) in a..b, Real.sin x ^ n) - (n + 1) * ∫ (x : ) in a..b, Real.sin x ^ (n + 2)
theorem integral_sin_pow {a : } {b : } (n : ) :
∫ (x : ) in a..b, Real.sin x ^ (n + 2) = (Real.sin a ^ (n + 1) * Real.cos a - Real.sin b ^ (n + 1) * Real.cos b) / (n + 2) + (n + 1) / (n + 2) * ∫ (x : ) in a..b, Real.sin x ^ n

The reduction formula for the integral of sin x ^ n for any natural n ≥ 2.

@[simp]
theorem integral_sin_sq {a : } {b : } :
∫ (x : ) in a..b, Real.sin x ^ 2 = (Real.sin a * Real.cos a - Real.sin b * Real.cos b + b - a) / 2
theorem integral_sin_pow_odd (n : ) :
∫ (x : ) in 0 ..Real.pi, Real.sin x ^ (2 * n + 1) = 2 * Finset.prod (Finset.range n) fun (i : ) => (2 * i + 2) / (2 * i + 3)
theorem integral_sin_pow_even (n : ) :
∫ (x : ) in 0 ..Real.pi, Real.sin x ^ (2 * n) = Real.pi * Finset.prod (Finset.range n) fun (i : ) => (2 * i + 1) / (2 * i + 2)
theorem integral_sin_pow_pos (n : ) :
0 < ∫ (x : ) in 0 ..Real.pi, Real.sin x ^ n
theorem integral_sin_pow_succ_le (n : ) :
∫ (x : ) in 0 ..Real.pi, Real.sin x ^ (n + 1) ∫ (x : ) in 0 ..Real.pi, Real.sin x ^ n
theorem integral_sin_pow_antitone :
Antitone fun (n : ) => ∫ (x : ) in 0 ..Real.pi, Real.sin x ^ n

Integral of cos x ^ n #

theorem integral_cos_pow_aux {a : } {b : } (n : ) :
∫ (x : ) in a..b, Real.cos x ^ (n + 2) = (Real.cos b ^ (n + 1) * Real.sin b - Real.cos a ^ (n + 1) * Real.sin a + (n + 1) * ∫ (x : ) in a..b, Real.cos x ^ n) - (n + 1) * ∫ (x : ) in a..b, Real.cos x ^ (n + 2)
theorem integral_cos_pow {a : } {b : } (n : ) :
∫ (x : ) in a..b, Real.cos x ^ (n + 2) = (Real.cos b ^ (n + 1) * Real.sin b - Real.cos a ^ (n + 1) * Real.sin a) / (n + 2) + (n + 1) / (n + 2) * ∫ (x : ) in a..b, Real.cos x ^ n

The reduction formula for the integral of cos x ^ n for any natural n ≥ 2.

@[simp]
theorem integral_cos_sq {a : } {b : } :
∫ (x : ) in a..b, Real.cos x ^ 2 = (Real.cos b * Real.sin b - Real.cos a * Real.sin a + b - a) / 2

Integral of sin x ^ m * cos x ^ n #

theorem integral_sin_pow_mul_cos_pow_odd {a : } {b : } (m : ) (n : ) :
∫ (x : ) in a..b, Real.sin x ^ m * Real.cos x ^ (2 * n + 1) = ∫ (u : ) in Real.sin a..Real.sin b, u ^ m * (1 - u ^ 2) ^ n

Simplification of the integral of sin x ^ m * cos x ^ n, case n is odd.

@[simp]
theorem integral_sin_mul_cos₁ {a : } {b : } :
∫ (x : ) in a..b, Real.sin x * Real.cos x = (Real.sin b ^ 2 - Real.sin a ^ 2) / 2

The integral of sin x * cos x, given in terms of sin². See integral_sin_mul_cos₂ below for the integral given in terms of cos².

@[simp]
theorem integral_sin_sq_mul_cos {a : } {b : } :
∫ (x : ) in a..b, Real.sin x ^ 2 * Real.cos x = (Real.sin b ^ 3 - Real.sin a ^ 3) / 3
@[simp]
theorem integral_cos_pow_three {a : } {b : } :
∫ (x : ) in a..b, Real.cos x ^ 3 = Real.sin b - Real.sin a - (Real.sin b ^ 3 - Real.sin a ^ 3) / 3
theorem integral_sin_pow_odd_mul_cos_pow {a : } {b : } (m : ) (n : ) :
∫ (x : ) in a..b, Real.sin x ^ (2 * m + 1) * Real.cos x ^ n = ∫ (u : ) in Real.cos b..Real.cos a, u ^ n * (1 - u ^ 2) ^ m

Simplification of the integral of sin x ^ m * cos x ^ n, case m is odd.

theorem integral_sin_mul_cos₂ {a : } {b : } :
∫ (x : ) in a..b, Real.sin x * Real.cos x = (Real.cos a ^ 2 - Real.cos b ^ 2) / 2

The integral of sin x * cos x, given in terms of cos². See integral_sin_mul_cos₁ above for the integral given in terms of sin².

@[simp]
theorem integral_sin_mul_cos_sq {a : } {b : } :
∫ (x : ) in a..b, Real.sin x * Real.cos x ^ 2 = (Real.cos a ^ 3 - Real.cos b ^ 3) / 3
@[simp]
theorem integral_sin_pow_three {a : } {b : } :
∫ (x : ) in a..b, Real.sin x ^ 3 = Real.cos a - Real.cos b - (Real.cos a ^ 3 - Real.cos b ^ 3) / 3
theorem integral_sin_pow_even_mul_cos_pow_even {a : } {b : } (m : ) (n : ) :
∫ (x : ) in a..b, Real.sin x ^ (2 * m) * Real.cos x ^ (2 * n) = ∫ (x : ) in a..b, ((1 - Real.cos (2 * x)) / 2) ^ m * ((1 + Real.cos (2 * x)) / 2) ^ n

Simplification of the integral of sin x ^ m * cos x ^ n, case m and n are both even.

@[simp]
theorem integral_sin_sq_mul_cos_sq {a : } {b : } :
∫ (x : ) in a..b, Real.sin x ^ 2 * Real.cos x ^ 2 = (b - a) / 8 - (Real.sin (4 * b) - Real.sin (4 * a)) / 32

Integral of misc. functions #

theorem integral_sqrt_one_sub_sq :
∫ (x : ) in -1 ..1, Real.sqrt (1 - x ^ 2) = Real.pi / 2