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
andcos x ^ n
forn ≥ 2
- The computation of
∫ x in 0..π, sin x ^ n
as a product for even and oddn
(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
interval_integral.interval_integrable_pow
{a b : ℝ}
(n : ℕ)
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ] :
interval_integrable (λ (x : ℝ), x ^ n) μ a b
theorem
interval_integral.interval_integrable_zpow
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
{n : ℤ}
(h : 0 ≤ n ∨ 0 ∉ set.interval a b) :
interval_integrable (λ (x : ℝ), x ^ n) μ a b
theorem
interval_integral.interval_integrable_rpow
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
{r : ℝ}
(h : 0 ≤ r ∨ 0 ∉ set.interval a b) :
interval_integrable (λ (x : ℝ), x ^ r) μ a b
theorem
interval_integral.interval_integrable_rpow'
{a b r : ℝ}
(h : -1 < r) :
interval_integrable (λ (x : ℝ), x ^ r) measure_theory.measure_space.volume a b
Alternative version with a weaker hypothesis on r
, but assuming the measure is volume.
theorem
interval_integral.interval_integrable_cpow
{a b : ℝ}
{r : ℂ}
(ha : 0 < a)
(hb : 0 < b) :
interval_integrable (λ (x : ℝ), ↑x ^ r) measure_theory.measure_space.volume a b
@[simp]
theorem
interval_integral.interval_integrable_id
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ] :
interval_integrable (λ (x : ℝ), x) μ a b
@[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
@[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.is_locally_finite_measure μ]
(h : ∀ (x : ℝ), x ∈ set.interval a b → f 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.is_locally_finite_measure μ]
(h : ∀ (x : ℝ), x ∈ set.interval a b → f x ≠ 0)
(hf : continuous_on f (set.interval a b)) :
interval_integrable (λ (x : ℝ), (f x)⁻¹) μ a b
@[simp]
theorem
interval_integral.interval_integrable_exp
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ] :
interval_integrable real.exp μ a b
@[simp]
theorem
interval_integral.interval_integrable.log
{a b : ℝ}
{f : ℝ → ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
(hf : continuous_on f (set.interval a b))
(h : ∀ (x : ℝ), x ∈ set.interval a b → f x ≠ 0) :
interval_integrable (λ (x : ℝ), real.log (f x)) μ a b
@[simp]
theorem
interval_integral.interval_integrable_log
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ]
(h : 0 ∉ set.interval a b) :
interval_integrable real.log μ a b
@[simp]
theorem
interval_integral.interval_integrable_sin
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ] :
interval_integrable real.sin μ a b
@[simp]
theorem
interval_integral.interval_integrable_cos
{a b : ℝ}
{μ : measure_theory.measure ℝ}
[measure_theory.is_locally_finite_measure μ] :
interval_integrable real.cos μ a b
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
@[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)
#
Integrals of simple functions #
@[simp]
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_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
Integral of sin x ^ n
#
The reduction formula for the integral of sin x ^ n
for any natural n ≥ 2
.
Integral of cos x ^ n
#
The reduction formula for the integral of cos x ^ n
for any natural n ≥ 2
.
Integral of sin x ^ m * cos x ^ n
#
Simplification of the integral of sin x ^ m * cos x ^ n
, case m
and n
are both even.