Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-19 23:44 ca827bae

View on Github →

feat(analysis/special_functions/compare_exp): new file (#16543) Prove (λ z, z ^ a * exp (b * z)) =o[l] λ z, z ^ a' * exp (b' * z) for an appropriate filter l, any complex a, a', and real b < b'.

Estimated changes