Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes