mathlib

ca827bae - feat(analysis/special_functions/compare_exp): new file (#16543)

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'`.