Theorems · Theorem · number theory

CuspFormClass.qExpansion_isBigO

∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ]
  [CuspFormClass F Γ k] (f : F),
  (fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) =O[Filter.atTop] fun n =>
    ↑n ^ (↑k / 2)

Hecke's bound for the coefficients of a cusp form: if f is a weight k modular form for an arithmetic subgroup, then its q-expansion coefficients are O (n ^ (k / 2)). This is not optimal -- the optimal exponent is (k - 1) / 2 + ε for any 0 < ε, at least for congruence levels -- but is much easier to prove than the optimal result.

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeCuspFormClass