Evaluation of specific improper integrals

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

See also

• 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 (Set.Iic c)

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)

If 0 < c, then (λ 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) ↔ s < -1

theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ s) (Set.Ioi 0)

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)

theorem integrableOn_Ioi_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ↑x ^ s) (Set.Ioi t) ↔ s.re < -1

theorem not_integrableOn_Ioi_cpow (s : ℂ) : ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => ↑x ^ s) (Set.Ioi 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)