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 .

These lemmas are stated in terms of either Iic or Ioi (neglecting Iio and Ici) to match mathlib's conventions for integrals over finite intervals (see intervalIntegral).

See also #

theorem integral_exp_mul_complex_Ioi {a : } (ha : a.re < 0) (c : ) :
(x : ) in Set.Ioi c, Complex.exp (a * x) = -Complex.exp (a * c) / a
theorem integral_exp_mul_complex_Iic {a : } (ha : 0 < a.re) (c : ) :
(x : ) in Set.Iic c, Complex.exp (a * x) = Complex.exp (a * c) / a
theorem integral_exp_mul_Ioi {a : } (ha : a < 0) (c : ) :
(x : ) in Set.Ioi c, Real.exp (a * x) = -Real.exp (a * c) / a
theorem integral_exp_mul_Iic {a : } (ha : 0 < a) (c : ) :
(x : ) in Set.Iic c, Real.exp (a * x) = Real.exp (a * c) / a
theorem integrableOn_Ioi_rpow_of_lt {a : } (ha : a < -1) {c : } (hc : 0 < c) :

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

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_norm_cpow_of_lt {a : } (ha : a.re < -1) {c : } (hc : 0 < c) :
theorem integrableOn_Ioi_cpow_of_lt {a : } (ha : a.re < -1) {c : } (hc : 0 < c) :
theorem integrableOn_Ioi_cpow_iff {s : } {t : } (ht : 0 < t) :
theorem integrableOn_Ioi_deriv_ofReal_cpow {s : } {t : } (ht : 0 < t) (hs : s.re < 0) :

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)
@[simp]
@[simp]