Theorems · Theorem · number theory

ModularFormClass.qExpansion_isBigO

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

Bound for the coefficients of a modular form: if f is a weight k modular form for an arithmetic subgroup, then its q-expansion coefficients are O (n ^ k). This is not optimal -- the optimal exponent is k - 1 + ε for any 0 < ε, at least for congruence levels -- but is much easier to prove than the optimal result. See CuspFormClass.qExpansion_isBigO for a sharper bound assuming f is cuspidal.

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeModularFormClass