mathlib3 documentation

analysis.special_functions.integrals

Integration of specific interval integrals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[simp]
theorem interval_integral.interval_integrable_pow {a b : ℝ} (n : ℕ) {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable (λ (x : ℝ), x ^ n) μ a b
source
theorem interval_integral.interval_integrable_zpow {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] {n : ℤ} (h : 0 ≤ n ∨ 0 ∉ set.uIcc a b) :
interval_integrable (λ (x : ℝ), x ^ n) μ a b
source
theorem interval_integral.interval_integrable_rpow {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] {r : ℝ} (h : 0 ≤ r ∨ 0 ∉ set.uIcc a b) :
interval_integrable (λ (x : ℝ), x ^ r) μ a b

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

source
theorem interval_integral.interval_integrable_rpow' {a b r : ℝ} (h : -1 < r) :
interval_integrable (λ (x : ℝ), x ^ r) measure_theory.measure_space.volume a b

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

source
theorem interval_integral.interval_integrable_cpow {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] {r : ℂ} (h : 0 ≤ r.re ∨ 0 ∉ set.uIcc a b) :
interval_integrable (λ (x : ℝ), ↑x ^ r) μ a b

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

source
theorem interval_integral.interval_integrable_cpow' {a b : ℝ} {r : ℂ} (h : -1 < r.re) :
interval_integrable (λ (x : ℝ), ↑x ^ r) measure_theory.measure_space.volume a b

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

source
@[simp]
theorem interval_integral.interval_integrable_id {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable (λ (x : ℝ), x) μ a b
source
@[simp]
theorem interval_integral.interval_integrable_const {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] (c : ℝ) :
interval_integrable (λ (x : ℝ), c) μ a b
source
theorem interval_integral.interval_integrable_one_div {a b : ℝ} {f : ℝ → ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] (h : ∀ (x : ℝ), x ∈ set.uIcc a b → f x ≠ 0) (hf : continuous_on f (set.uIcc a b)) :
interval_integrable (λ (x : ℝ), 1 / f x) μ a b
source
@[simp]
theorem interval_integral.interval_integrable_inv {a b : ℝ} {f : ℝ → ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] (h : ∀ (x : ℝ), x ∈ set.uIcc a b → f x ≠ 0) (hf : continuous_on f (set.uIcc a b)) :
interval_integrable (λ (x : ℝ), (f x)⁻¹) μ a b
source
@[simp]
theorem interval_integral.interval_integrable_exp {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable rexp μ a b
source
@[simp]
theorem interval_integrable.log {a b : ℝ} {f : ℝ → ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] (hf : continuous_on f (set.uIcc a b)) (h : ∀ (x : ℝ), x ∈ set.uIcc a b → f x ≠ 0) :
interval_integrable (λ (x : ℝ), real.log (f x)) μ a b
source
@[simp]
theorem interval_integral.interval_integrable_log {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] (h : 0 ∉ set.uIcc a b) :
interval_integrable real.log μ a b
source
@[simp]
theorem interval_integral.interval_integrable_sin {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable real.sin μ a b
source
@[simp]
theorem interval_integral.interval_integrable_cos {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable real.cos μ a b
source
theorem interval_integral.interval_integrable_one_div_one_add_sq {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable (λ (x : ℝ), 1 / (1 + x ^ 2)) μ a b
source
@[simp]
theorem interval_integral.interval_integrable_inv_one_add_sq {a b : ℝ} {μ : measure_theory.measure ℝ} [measure_theory.is_locally_finite_measure μ] :
interval_integrable (λ (x : ℝ), (1 + x ^ 2)⁻¹) μ a b

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

source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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
source
@[simp]
theorem interval_integral.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 #

source
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)
source
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)
source
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)
source
@[simp]
theorem integral_pow {a b : ℝ} (n : ℕ) :
∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
source
theorem integral_pow_abs_sub_uIoc {a b : ℝ} (n : ℕ) :
∫ (x : ℝ) in set.uIoc 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.

source
@[simp]
theorem integral_id {a b : ℝ} :
∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
source
@[simp]
theorem integral_one {a b : ℝ} :
∫ (x : ℝ) in a..b, 1 = b - a
source
theorem integral_const_on_unit_interval {a b : ℝ} :
∫ (x : ℝ) in a..a + 1, b = b
source
@[simp]
theorem integral_inv {a b : ℝ} (h : 0 ∉ set.uIcc a b) :
∫ (x : ℝ) in a..b, x⁻¹ = real.log (b / a)
source
@[simp]
theorem integral_inv_of_pos {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
∫ (x : ℝ) in a..b, x⁻¹ = real.log (b / a)
source
@[simp]
theorem integral_inv_of_neg {a b : ℝ} (ha : a < 0) (hb : b < 0) :
∫ (x : ℝ) in a..b, x⁻¹ = real.log (b / a)
source
theorem integral_one_div {a b : ℝ} (h : 0 ∉ set.uIcc a b) :
∫ (x : ℝ) in a..b, 1 / x = real.log (b / a)
source
theorem integral_one_div_of_pos {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
∫ (x : ℝ) in a..b, 1 / x = real.log (b / a)
source
theorem integral_one_div_of_neg {a b : ℝ} (ha : a < 0) (hb : b < 0) :
∫ (x : ℝ) in a..b, 1 / x = real.log (b / a)
source
@[simp]
theorem integral_exp {a b : ℝ} :
∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a
source
theorem integral_exp_mul_complex {a b : ℝ} {c : ℂ} (hc : c ≠ 0) :
∫ (x : ℝ) in a..b, cexp (c * ↑x) = (cexp (c * ↑b) - cexp (c * ↑a)) / c
source
@[simp]
theorem integral_log {a b : ℝ} (h : 0 ∉ set.uIcc a b) :
∫ (x : ℝ) in a..b, real.log x = b * real.log b - a * real.log a - b + a
source
@[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
source
@[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
source
@[simp]
theorem integral_sin {a b : ℝ} :
∫ (x : ℝ) in a..b, real.sin x = real.cos a - real.cos b
source
@[simp]
theorem integral_cos {a b : ℝ} :
∫ (x : ℝ) in a..b, real.cos x = real.sin b - real.sin a
source
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
source
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
source
@[simp]
theorem integral_inv_one_add_sq {a b : ℝ} :
∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = real.arctan b - real.arctan a
source
theorem integral_one_div_one_add_sq {a b : ℝ} :
∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = real.arctan b - real.arctan a
source
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))
source
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 #

source
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)
source
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.

source
@[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
source
theorem integral_sin_pow_odd (n : ℕ) :
∫ (x : ℝ) in 0..real.pi, real.sin x ^ (2 * n + 1) = 2 * (finset.range n).prod (λ (i : ℕ), (2 * ↑i + 2) / (2 * ↑i + 3))
source
theorem integral_sin_pow_even (n : ℕ) :
∫ (x : ℝ) in 0..real.pi, real.sin x ^ (2 * n) = real.pi * (finset.range n).prod (λ (i : ℕ), (2 * ↑i + 1) / (2 * ↑i + 2))
source
theorem integral_sin_pow_pos (n : ℕ) :
0 < ∫ (x : ℝ) in 0..real.pi, real.sin x ^ n
source
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
source
theorem integral_sin_pow_antitone  :
antitone (λ (n : ℕ), ∫ (x : ℝ) in 0..real.pi, real.sin x ^ n)

Integral of cos x ^ n #

source
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)
source
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.

source
@[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 #

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

source
@[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².

source
@[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
source
@[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
source
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.

source
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².

source
@[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
source
@[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
source
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.

source
@[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