mathlib3 documentation

analysis.special_functions.improper_integrals

Evaluation of specific improper integrals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

See also #

source
theorem integrable_on_exp_Iic (c : ℝ) :
measure_theory.integrable_on rexp (set.Iic c) measure_theory.measure_space.volume
source
theorem integral_exp_Iic (c : ℝ) :
∫ (x : ℝ) in set.Iic c, rexp x = rexp c
source
theorem integral_exp_Iic_zero  :
∫ (x : ℝ) in set.Iic 0, rexp x = 1
source
theorem integral_exp_neg_Ioi (c : ℝ) :
∫ (x : ℝ) in set.Ioi c, rexp (-x) = rexp (-c)
source
theorem integral_exp_neg_Ioi_zero  :
∫ (x : ℝ) in set.Ioi 0, rexp (-x) = 1
source
theorem integrable_on_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :
measure_theory.integrable_on (λ (t : ℝ), t ^ a) (set.Ioi c) measure_theory.measure_space.volume

If 0 < c, then (λ t : ℝ, t ^ a) is integrable on (c, ∞) for all a < -1.

source
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)
source
theorem integrable_on_Ioi_cpow_of_lt {a : ℂ} (ha : a.re < -1) {c : ℝ} (hc : 0 < c) :
measure_theory.integrable_on (λ (t : ℝ), ↑t ^ a) (set.Ioi c) measure_theory.measure_space.volume
source
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)