mathlib
ec452806 - feat(analysis/special_functions): file for evaluations of specific improper integrals (#18821)

Commit
2 years ago
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)`). Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading