Theorem cexp_neg_quadratic_isLittleO_rpow_atTop

Modification history

2024-04-15 06:46

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

refactor(SpecialFunctions/Gaussian): shorten long pole (#12104) …

Modified cexp_neg_quadratic_isLittleO_rpow_atTop View on Github →

2024-01-17 14:32

Mathlib/Analysis/SpecialFunctions/Gaussian.lean

feat(NumberTheory/ModularForms): two-variable Jacobi theta (#9666) …

Added cexp_neg_quadratic_isLittleO_rpow_atTop View on Github →