Mathlib Changelog
v4
Changelog
About
Github
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