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 #

theorem integral_exp_Iic (c : ) :
(x : ) in set.Iic c, rexp x = rexp c
theorem integral_exp_Iic_zero  :
(x : ) in set.Iic 0, rexp x = 1
theorem integral_exp_neg_Ioi (c : ) :
(x : ) in set.Ioi c, rexp (-x) = rexp (-c)
theorem integrable_on_Ioi_rpow_of_lt {a : } (ha : a < -1) {c : } (hc : 0 < 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 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)