Evaluation of specific improper integrals

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

See also

• analysis.special_functions.integrals -- integrals over finite intervals
• analysis.special_functions.gaussian -- integral of exp (-x ^ 2)
• analysis.special_functions.japanese_bracket-- 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 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 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)