Commit 2023-06-09 23:11 d9c7687b

View on Github →

feat: port Analysis.SpecialFunctions.ImproperIntegrals (#4928)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

added theorem integrableOn_Ioi_cpow_of_lt

added theorem integrableOn_Ioi_rpow_of_lt

added theorem integrableOn_exp_Iic

added theorem integral_Ioi_cpow_of_lt

added theorem integral_Ioi_rpow_of_lt

added theorem integral_exp_Iic

added theorem integral_exp_Iic_zero

added theorem integral_exp_neg_Ioi

added theorem integral_exp_neg_Ioi_zero