Commit 2023-05-03 03:14 ec452806
View on Github →feat(analysis/special_functions): file for evaluations of specific improper integrals (#18821)
We have the file analysis/special_functions/integrals.lean
which has numerous evaluations of interval integrals. This adds a counterpart file for integrals over infinite intervals.
(Added as preparation for a forthcoming PR about Mellin transforms -- I wanted somewhere to put the fact that x ^ (-a)
is integrable on [1, infinity)
).