# mathlib3documentation

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 ℝ.

• 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 integral_exp_Iic (c : ) :
(x : ) in , rexp x = rexp c
theorem integral_exp_Iic_zero  :
(x : ) in , rexp x = 1
theorem integral_exp_neg_Ioi (c : ) :
(x : ) in , rexp (-x) = rexp (-c)
theorem integral_exp_neg_Ioi_zero  :
(x : ) in , rexp (-x) = 1
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 , t ^ a = -c ^ (a + 1) / (a + 1)
theorem integral_Ioi_cpow_of_lt {a : } (ha : a.re < -1) {c : } (hc : 0 < c) :
(t : ) in , t ^ a = -c ^ (a + 1) / (a + 1)