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) MeasureTheory.volume

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 integrableAtFilter_rpow_atTop_iff {s : ℝ} : MeasureTheory.IntegrableAtFilter (fun (x : ℝ) => x ^ s) Filter.atTop 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_norm_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_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_norm_cpow_iff {s : ℂ} {t : ℝ} (ht : 0 < t) : MeasureTheory.IntegrableOn (fun (x : ℝ) => ‖↑x ^ s‖) (Set.Ioi t) MeasureTheory.volume ↔ s.re < -1

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 integrableOn_Ioi_deriv_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re < 0) : MeasureTheory.IntegrableOn (deriv fun (x : ℝ) => ↑x ^ s) (Set.Ioi t) MeasureTheory.volume

theorem integrableOn_Ioi_deriv_norm_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re ≤ 0) : MeasureTheory.IntegrableOn (deriv fun (x : ℝ) => ‖↑x ^ s‖) (Set.Ioi t) MeasureTheory.volume

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