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

• Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean: specific integrals over finite intervals
• Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean: integral of exp (-x ^ 2)
• Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean: integrability of (1+‖x‖)^(-r).

theorem integrableOn_exp_Iic (c : ℝ) : MeasureTheory.IntegrableOn Real.exp (Set.Iic c) MeasureTheory.volume

theorem integrableOn_exp_neg_Ioi (c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-x)) (Set.Ioi 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_exp_mul_complex_Ioi {a : ℂ} (ha : a.re < 0) (c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp (a * ↑x)) (Set.Ioi c) MeasureTheory.volume

theorem integrableOn_exp_mul_complex_Iic {a : ℂ} (ha : 0 < a.re) (c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp (a * ↑x)) (Set.Iic c) MeasureTheory.volume

theorem integrableOn_exp_mul_Ioi {a : ℝ} (ha : a < 0) (c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (a * x)) (Set.Ioi c) MeasureTheory.volume

theorem integrableOn_exp_mul_Iic {a : ℝ} (ha : 0 < a) (c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (a * x)) (Set.Iic c) MeasureTheory.volume

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_add_rpow_Ioi_of_lt {a c m : ℝ} (ha : a < -1) (hc : -m < c) : MeasureTheory.IntegrableOn (fun (x : ℝ) => (x + m) ^ a) (Set.Ioi c) MeasureTheory.volume

If -m < c, then (fun t : ℝ ↦ (t + m) ^ a) is integrable on (c, ∞) for all a < -1.

theorem integrableOn_Ioi_rpow_of_lt {a c : ℝ} (ha : a < -1) (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