Documentation

Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Evaluation of specific improper integrals #

This file contains some integrability results, and evaluations of integrals, over or over half-infinite intervals in .

See also #

theorem integral_exp_Iic (c : ) :
∫ (x : ) in Set.Iic c, Real.exp x = Real.exp c
theorem integral_exp_Iic_zero :
∫ (x : ) in Set.Iic 0, Real.exp x = 1
theorem integral_exp_neg_Ioi (c : ) :
∫ (x : ) in Set.Ioi c, Real.exp (-x) = Real.exp (-c)
theorem integral_exp_neg_Ioi_zero :
∫ (x : ) in Set.Ioi 0, Real.exp (-x) = 1
theorem integrableOn_Ioi_rpow_of_lt {a : } (ha : a < -1) {c : } (hc : 0 < c) :
MeasureTheory.IntegrableOn (fun (t : ) => t ^ a) (Set.Ioi c) MeasureTheory.volume

If 0 < c, then (fun t : ℝ ↦ t ^ a) is integrable on (c, ∞) for all a < -1.

theorem integrableOn_Ioi_rpow_iff {s : } {t : } (ht : 0 < t) :
MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) (Set.Ioi t) MeasureTheory.volume s < -1
theorem not_integrableOn_Ioi_rpow (s : ) :
¬MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) (Set.Ioi 0) MeasureTheory.volume

The real power function with any exponent is not integrable on (0, +∞).

theorem setIntegral_Ioi_zero_rpow (s : ) :
∫ (x : ) in Set.Ioi 0, x ^ s = 0
theorem integral_Ioi_rpow_of_lt {a : } (ha : a < -1) {c : } (hc : 0 < c) :
∫ (t : ) in Set.Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
theorem integrableOn_Ioi_cpow_of_lt {a : } (ha : a.re < -1) {c : } (hc : 0 < c) :
MeasureTheory.IntegrableOn (fun (t : ) => t ^ a) (Set.Ioi c) MeasureTheory.volume
theorem integrableOn_Ioi_cpow_iff {s : } {t : } (ht : 0 < t) :
MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) (Set.Ioi t) MeasureTheory.volume s.re < -1
theorem not_integrableOn_Ioi_cpow (s : ) :
¬MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) (Set.Ioi 0) MeasureTheory.volume

The complex power function with any exponent is not integrable on (0, +∞).

theorem setIntegral_Ioi_zero_cpow (s : ) :
∫ (x : ) in Set.Ioi 0, x ^ s = 0
theorem integral_Ioi_cpow_of_lt {a : } (ha : a.re < -1) {c : } (hc : 0 < c) :
∫ (t : ) in Set.Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
theorem integrable_inv_one_add_sq :
MeasureTheory.Integrable (fun (x : ) => (1 + x ^ 2)⁻¹) MeasureTheory.volume
@[simp]
theorem integral_Iic_inv_one_add_sq {i : } :
∫ (x : ) in Set.Iic i, (1 + x ^ 2)⁻¹ = Real.arctan i + Real.pi / 2
@[simp]
theorem integral_Ioi_inv_one_add_sq {i : } :
∫ (x : ) in Set.Ioi i, (1 + x ^ 2)⁻¹ = Real.pi / 2 - Real.arctan i
@[simp]
theorem integral_univ_inv_one_add_sq :
∫ (x : ), (1 + x ^ 2)⁻¹ = Real.pi