Theorems · Theorem · number theory

qExpansion_coeff_isBigO_of_norm_isBigO

∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
  [ModularFormClass F Γ k] (f : F) (e : ℝ),
  (⇑f =O[Filter.comap UpperHalfPlane.im (nhds 0)] fun τ => τ.im ^ (-e)) →
    (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) =O[Filter.atTop] fun n => ↑n ^ e

General result on bounding q-expansion coefficients using a bound on the norm of the function. This will get used twice over, once for cusp forms (with e = k / 2) and once for modular forms (with e = k).

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

2 results in Mathlib

Foundations

Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Subgroup.IsArithmeticFunLikeModularFormClass