mathlib documentation

analysis.special_functions.integrals

Integration of specific interval integrals #

This file contains proofs of the integrals of various simple functions, including pow, exp, inv/one_div, sin, cos, and λ x, 1 / (1 + x^2).

There are also facts about more complicated integrals:

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

This file is still being developed.

@[simp]
theorem interval_integral.integral_const_mul {a b : } {f : } (c : ) :
∫ (x : ) in a..b, c * f x = c * ∫ (x : ) in a..b, f x
@[simp]
theorem interval_integral.integral_mul_const {a b : } {f : } (c : ) :
∫ (x : ) in a..b, (f x) * c = (∫ (x : ) in a..b, f x) * c
@[simp]
theorem interval_integral.integral_div {a b : } {f : } (c : ) :
∫ (x : ) in a..b, f x / c = (∫ (x : ) in a..b, f x) / c
@[simp]
theorem interval_integral.interval_integrable.const_mul {a b : } {f : } {ν : measure_theory.measure } (c : ) (h : interval_integrable f ν a b) :
interval_integrable (λ (x : ), c * f x) ν a b
@[simp]
theorem interval_integral.interval_integrable.mul_const {a b : } {f : } {ν : measure_theory.measure } (c : ) (h : interval_integrable f ν a b) :
interval_integrable (λ (x : ), (f x) * c) ν a b
@[simp]
theorem interval_integral.interval_integrable.div {a b : } {f : } {ν : measure_theory.measure } (c : ) (h : interval_integrable f ν a b) :
interval_integrable (λ (x : ), f x / c) ν a b
theorem interval_integral.interval_integrable_one_div {a b : } {f : } {μ : measure_theory.measure } [measure_theory.locally_finite_measure μ] (h : ∀ (x : ), x set.interval a bf x 0) (hf : continuous_on f (set.interval a b)) :
interval_integrable (λ (x : ), 1 / f x) μ a b
@[simp]
theorem interval_integral.interval_integrable_inv {a b : } {f : } {μ : measure_theory.measure } [measure_theory.locally_finite_measure μ] (h : ∀ (x : ), x set.interval a bf x 0) (hf : continuous_on f (set.interval a b)) :
interval_integrable (λ (x : ), (f x)⁻¹) μ a b
@[simp]
theorem integral_pow {a b : } (n : ) :
∫ (x : ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1)
@[simp]
theorem integral_id {a b : } :
∫ (x : ) in a..b, x = (b ^ 2 - a ^ 2) / 2
@[simp]
theorem integral_one {a b : } :
∫ (x : ) in a..b, 1 = b - a
@[simp]
theorem integral_exp {a b : } :
∫ (x : ) in a..b, real.exp x = real.exp b - real.exp a
@[simp]
theorem integral_inv {a b : } (h : 0 set.interval 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 : 0 set.interval 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_sin {a b : } :
∫ (x : ) in a..b, real.sin x = real.cos a - real.cos b
theorem integral_sin_pow_aux (n : ) :
∫ (x : ) in 0..π, real.sin x ^ (n + 2) = ((n + 1) * ∫ (x : ) in 0..π, real.sin x ^ n) - (n + 1) * ∫ (x : ) in 0..π, real.sin x ^ (n + 2)
theorem integral_sin_pow_succ_succ (n : ) :
∫ (x : ) in 0..π, real.sin x ^ (n + 2) = ((n + 1) / (n + 2)) * ∫ (x : ) in 0..π, real.sin x ^ n
theorem integral_sin_pow_odd (n : ) :
∫ (x : ) in 0..π, real.sin x ^ (2 * n + 1) = 2 * ∏ (i : ) in finset.range n, (2 * i + 2) / (2 * i + 3)
theorem integral_sin_pow_even (n : ) :
∫ (x : ) in 0..π, real.sin x ^ 2 * n = π * ∏ (i : ) in finset.range n, (2 * i + 1) / (2 * i + 2)
theorem integral_sin_pow_pos (n : ) :
0 < ∫ (x : ) in 0..π, real.sin x ^ n
@[simp]
theorem integral_cos {a b : } :
∫ (x : ) in a..b, real.cos x = real.sin b - real.sin a
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
@[simp]
theorem integral_inv_one_add_sq {a b : } :
∫ (x : ) in a..b, (1 + x ^ 2)⁻¹ = real.arctan b - real.arctan a
theorem integral_one_div_one_add_sq {a b : } :
∫ (x : ) in a..b, 1 / (1 + x ^ 2) = real.arctan b - real.arctan a