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) :

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

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