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 intervalsanalysis.special_functions.gaussian
-- integral ofexp (-x ^ 2)
analysis.special_functions.japanese_bracket
-- integrability of(1+‖x‖)^(-r)
.
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
integrableOn_Ioi_cpow_of_lt
{a : ℂ}
(ha : a.re < -1)
{c : ℝ}
(hc : 0 < c)
:
MeasureTheory.IntegrableOn (fun t => ↑t ^ a) (Set.Ioi c)