English
Let f be a cusp form of weight k for Γ(n). Then f decays exponentially toward the cusp at infinity: as Im(τ) → ∞, f(τ) is bounded by a constant times exp(-2π Im(τ)/n).
Русский
Пусть f — вид cusp-функция весом k для Γ(n). Тогда f экспоненциально затухает при стыке к бесконечности: при Im(τ) → ∞ существует константа C так, что f(τ) = O(exp(-2π Im(τ)/n)).
LaTeX
$$$ f = O_{\operatorname{atImInfty}} \left( \tau \mapsto e^{-2\pi \operatorname{Im}(\tau)/n} \right) $$$
Lean4
theorem exp_decay_atImInfty [NeZero n] [CuspFormClass F Γ(n) k] :
f =O[atImInfty] fun τ ↦ Real.exp (-2 * π * τ.im / n) := by
simpa only [neg_mul, comp_def, ofComplex_apply, coe_im] using
((periodic_comp_ofComplex n f).exp_decay_of_zero_at_inf (mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _)))
(eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0)) fun _ ↦ differentiableAt_comp_ofComplex f)
(zero_at_infty_comp_ofComplex f)).comp_tendsto
tendsto_coe_atImInfty
