# Evaluation of specific improper integrals #

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

• Mathlib.Analysis.SpecialFunctions.Integrals -- integrals over finite intervals
• Mathlib.Analysis.SpecialFunctions.Gaussian -- integral of exp (-x ^ 2)
• Mathlib.Analysis.SpecialFunctions.JapaneseBracket-- integrability of (1+‖x‖)^(-r).
theorem integrableOn_exp_Iic (c : ) :
MeasureTheory.IntegrableOn Real.exp () MeasureTheory.volume
theorem integral_exp_Iic (c : ) :
∫ (x : ) in , x.exp = c.exp
theorem integral_exp_Iic_zero :
∫ (x : ) in , x.exp = 1
theorem integral_exp_neg_Ioi (c : ) :
∫ (x : ) in , (-x).exp = (-c).exp
theorem integral_exp_neg_Ioi_zero :
∫ (x : ) in , (-x).exp = 1
theorem integrableOn_Ioi_rpow_of_lt {a : } (ha : a < -1) {c : } (hc : 0 < c) :
MeasureTheory.IntegrableOn (fun (t : ) => t ^ a) () 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) () MeasureTheory.volume s < -1
theorem not_integrableOn_Ioi_rpow (s : ) :
¬MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) () MeasureTheory.volume

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

theorem setIntegral_Ioi_zero_rpow (s : ) :
∫ (x : ) in , x ^ s = 0
theorem integral_Ioi_rpow_of_lt {a : } (ha : a < -1) {c : } (hc : 0 < c) :
∫ (t : ) in , 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) () MeasureTheory.volume
theorem integrableOn_Ioi_cpow_iff {s : } {t : } (ht : 0 < t) :
MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) () MeasureTheory.volume s.re < -1
theorem not_integrableOn_Ioi_cpow (s : ) :
¬MeasureTheory.IntegrableOn (fun (x : ) => x ^ s) () MeasureTheory.volume

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

theorem setIntegral_Ioi_zero_cpow (s : ) :
∫ (x : ) in , x ^ s = 0
theorem integral_Ioi_cpow_of_lt {a : } (ha : a.re < -1) {c : } (hc : 0 < c) :
∫ (t : ) in , t ^ a = -c ^ (a + 1) / (a + 1)