Integration of specific interval integrals

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

• Integrals of simple functions, such as id, pow, inv, exp, log
• Integrals of some trigonometric functions, such as sin, cos, 1 / (1 + x^2)
• The integral of cos x ^ 2 - sin x ^ 2
• Reduction formulae for the integrals of sin x ^ n and cos x ^ n for n ≥ 2
• The computation of ∫ x in 0..π, sin x ^ n as a product for even and odd n (used in proving the Wallis product for pi)
• Integrals of the form sin x ^ m * cos x ^ n

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

@[simp]

theorem intervalIntegral.intervalIntegrable_pow {a : ℝ} {b : ℝ} (n : ℕ) {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => x ^ n) μ a b

theorem intervalIntegral.intervalIntegrable_zpow {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {n : ℤ} (h : 0 ≤ n ∨ 0 ∉ Set.uIcc a b) : IntervalIntegrable (fun (x : ℝ) => x ^ n) μ a b

theorem intervalIntegral.intervalIntegrable_rpow {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℝ} (h : 0 ≤ r ∨ 0 ∉ Set.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 ∨ 0 ∉ Set.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.

@[simp]

theorem intervalIntegral.intervalIntegrable_id {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => x) μ a b

theorem intervalIntegral.intervalIntegrable_const {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (c : ℝ) : IntervalIntegrable (fun (x : ℝ) => c) μ a b

theorem intervalIntegral.intervalIntegrable_one_div {a : ℝ} {b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ x ∈ Set.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 : ∀ x ∈ Set.uIcc a b, f x ≠ 0) (hf : ContinuousOn f (Set.uIcc a b)) : IntervalIntegrable (fun (x : ℝ) => (f x)⁻¹) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_exp {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable Real.exp μ a b

@[simp]

theorem IntervalIntegrable.log {a : ℝ} {b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (hf : ContinuousOn f (Set.uIcc a b)) (h : ∀ x ∈ Set.uIcc a b, f x ≠ 0) : IntervalIntegrable (fun (x : ℝ) => (f x).log) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_log {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (h : 0 ∉ Set.uIcc a b) : IntervalIntegrable Real.log μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_sin {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable Real.sin μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_cos {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable Real.cos μ a b

theorem intervalIntegral.intervalIntegrable_one_div_one_add_sq {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => 1 / (1 + x ^ 2)) μ a b

@[simp]

theorem intervalIntegral.intervalIntegrable_inv_one_add_sq {a : ℝ} {b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] : IntervalIntegrable (fun (x : ℝ) => (1 + x ^ 2)⁻¹) μ 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 ∧ 0 ∉ Set.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 ∧ 0 ∉ Set.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 ∧ 0 ∉ Set.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 : 0 ∉ Set.uIcc a b) : ∫ (x : ℝ) in a..b, x⁻¹ = (b / a).log

@[simp]

theorem integral_inv_of_pos {a : ℝ} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (x : ℝ) in a..b, x⁻¹ = (b / a).log

@[simp]

theorem integral_inv_of_neg {a : ℝ} {b : ℝ} (ha : a < 0) (hb : b < 0) : ∫ (x : ℝ) in a..b, x⁻¹ = (b / a).log

theorem integral_one_div {a : ℝ} {b : ℝ} (h : 0 ∉ Set.uIcc a b) : ∫ (x : ℝ) in a..b, 1 / x = (b / a).log

theorem integral_one_div_of_pos {a : ℝ} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (x : ℝ) in a..b, 1 / x = (b / a).log

theorem integral_one_div_of_neg {a : ℝ} {b : ℝ} (ha : a < 0) (hb : b < 0) : ∫ (x : ℝ) in a..b, 1 / x = (b / a).log

@[simp]

theorem integral_exp {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, x.exp = b.exp - a.exp

theorem integral_exp_mul_complex {a : ℝ} {b : ℝ} {c : ℂ} (hc : c ≠ 0) : ∫ (x : ℝ) in a..b, (c * ↑x).exp = ((c * ↑b).exp - (c * ↑a).exp) / c

@[simp]

theorem integral_log {a : ℝ} {b : ℝ} (h : 0 ∉ Set.uIcc a b) : ∫ (x : ℝ) in a..b, x.log = b * b.log - a * a.log - b + a

@[simp]

theorem integral_log_of_pos {a : ℝ} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (x : ℝ) in a..b, x.log = b * b.log - a * a.log - b + a

@[simp]

theorem integral_log_of_neg {a : ℝ} {b : ℝ} (ha : a < 0) (hb : b < 0) : ∫ (x : ℝ) in a..b, x.log = b * b.log - a * a.log - b + a

@[simp]

theorem integral_sin {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, x.sin = a.cos - b.cos

@[simp]

theorem integral_cos {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, x.cos = b.sin - a.sin

theorem integral_cos_mul_complex {z : ℂ} (hz : z ≠ 0) (a : ℝ) (b : ℝ) : ∫ (x : ℝ) in a..b, (z * ↑x).cos = (z * ↑b).sin / z - (z * ↑a).sin / z

theorem integral_cos_sq_sub_sin_sq {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, x.cos ^ 2 - x.sin ^ 2 = b.sin * b.cos - a.sin * a.cos

theorem integral_one_div_one_add_sq {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = b.arctan - a.arctan

@[simp]

theorem integral_inv_one_add_sq {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = b.arctan - a.arctan

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, x.sin ^ (n + 2) = (a.sin ^ (n + 1) * a.cos - b.sin ^ (n + 1) * b.cos + (↑n + 1) * ∫ (x : ℝ) in a..b, x.sin ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, x.sin ^ (n + 2)

theorem integral_sin_pow {a : ℝ} {b : ℝ} (n : ℕ) : ∫ (x : ℝ) in a..b, x.sin ^ (n + 2) = (a.sin ^ (n + 1) * a.cos - b.sin ^ (n + 1) * b.cos) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, x.sin ^ 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, x.sin ^ 2 = (a.sin * a.cos - b.sin * b.cos + b - a) / 2

theorem integral_sin_pow_odd (n : ℕ) : ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ (2 * n + 1) = 2 * (Finset.range n).prod fun (i : ℕ) => (2 * ↑i + 2) / (2 * ↑i + 3)

theorem integral_sin_pow_even (n : ℕ) : ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ (2 * n) = Real.pi * (Finset.range n).prod fun (i : ℕ) => (2 * ↑i + 1) / (2 * ↑i + 2)

theorem integral_sin_pow_pos (n : ℕ) : 0 < ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n

theorem integral_sin_pow_succ_le (n : ℕ) : ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n

theorem integral_sin_pow_antitone : Antitone fun (n : ℕ) => ∫ (x : ℝ) in 0 ..Real.pi, x.sin ^ n

Integral of cos x ^ n

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

theorem integral_cos_pow {a : ℝ} {b : ℝ} (n : ℕ) : ∫ (x : ℝ) in a..b, x.cos ^ (n + 2) = (b.cos ^ (n + 1) * b.sin - a.cos ^ (n + 1) * a.sin) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, x.cos ^ 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, x.cos ^ 2 = (b.cos * b.sin - a.cos * a.sin + 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, x.sin ^ m * x.cos ^ (2 * n + 1) = ∫ (u : ℝ) in a.sin..b.sin, 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, x.sin * x.cos = (b.sin ^ 2 - a.sin ^ 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, x.sin ^ 2 * x.cos = (b.sin ^ 3 - a.sin ^ 3) / 3

@[simp]

theorem integral_cos_pow_three {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, x.cos ^ 3 = b.sin - a.sin - (b.sin ^ 3 - a.sin ^ 3) / 3

theorem integral_sin_pow_odd_mul_cos_pow {a : ℝ} {b : ℝ} (m : ℕ) (n : ℕ) : ∫ (x : ℝ) in a..b, x.sin ^ (2 * m + 1) * x.cos ^ n = ∫ (u : ℝ) in b.cos..a.cos, 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, x.sin * x.cos = (a.cos ^ 2 - b.cos ^ 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, x.sin * x.cos ^ 2 = (a.cos ^ 3 - b.cos ^ 3) / 3

@[simp]

theorem integral_sin_pow_three {a : ℝ} {b : ℝ} : ∫ (x : ℝ) in a..b, x.sin ^ 3 = a.cos - b.cos - (a.cos ^ 3 - b.cos ^ 3) / 3

theorem integral_sin_pow_even_mul_cos_pow_even {a : ℝ} {b : ℝ} (m : ℕ) (n : ℕ) : ∫ (x : ℝ) in a..b, x.sin ^ (2 * m) * x.cos ^ (2 * n) = ∫ (x : ℝ) in a..b, ((1 - (2 * x).cos) / 2) ^ m * ((1 + (2 * x).cos) / 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, x.sin ^ 2 * x.cos ^ 2 = (b - a) / 8 - ((4 * b).sin - (4 * a).sin) / 32

Integral of misc. functions

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