Bounds for the norm of a modular form

We prove bounds for the norm of a modular form f τ in terms of im τ, and deduce polynomial bounds for its q-expansion coefficients. The main results are

• ModularFormClass.exists_bound: a modular form of weight k (for an arithmetic subgroup Γ) is bounded by a constant multiple of max 1 (1 / (im τ) ^ k)).
• CuspFormClass.exists_bound: a cusp form of weight k (for an arithmetic subgroup Γ) is bounded by a constant multiple of 1 / (im τ) ^ (k / 2).
• ModularFormClass.qExpansion_isBigO: for a a modular form of weight k (for an arithmetic subgroup Γ), the n-th q-expansion coefficient is O(n ^ k).
• CuspFormClass.qExpansion_isBigO: Hecke's bound for a a cusp form of weight k (for an arithmetic subgroup Γ): the n-th q-expansion coefficient is O(n ^ (k / 2)).

theorem ModularGroup.exists_bound_fundamental_domain_of_isBigO {E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) {t : ℝ} (hf_infinity : f =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => z.im ^ t) : ∃ (F : ℝ), ∀ τ ∈ fd, ‖f τ‖ ≤ F * τ.im ^ t

theorem ModularGroup.exists_bound_of_invariant_of_isBigO {E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) {t : ℝ} (ht : 0 ≤ t) (hf_infinity : f =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => z.im ^ t) (hf_inv : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), f (g • τ) = f τ) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

A function on ℍ which is invariant under SL(2, ℤ), and is O ((im τ) ^ t) at I∞ for some 0 ≤ t, is bounded on ℍ by a constant multiple of (max (im τ) (1 / im τ)) ^ t.

This will be applied to f τ * (im τ) ^ (k / 2) for f a modular form of weight k, taking t = 0 if f is cuspidal, and t = k / 2 otherwise.

theorem ModularGroup.exists_bound_of_subgroup_invariant_of_isBigO {E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) {t : ℝ} (ht : 0 ≤ t) (hf_infinity : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), (fun (τ : UpperHalfPlane) => f (g • τ)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => z.im ^ t) {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] (hf_inv : ∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

A function on ℍ which is invariant under a finite-index subgroup of SL(2, ℤ), and satisfies an O((im τ) ^ t) bound at all cusps for some 0 ≤ t, is in fact uniformly bounded by a multiple of (max (im τ) (1 / im τ)) ^ t.

theorem ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO {E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) {t : ℝ} (ht : 0 ≤ t) (hf_infinity : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), (fun (τ : UpperHalfPlane) => f (g • τ)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => z.im ^ t) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] (hf_inv : ∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

A function on ℍ which is invariant under an arithmetic subgroup of GL(2, ℝ), and satisfies an O((im τ) ^ t) bound at all cusps for some 0 ≤ t, is in fact uniformly bounded by a multiple of (max (im τ) (1 / im τ)) ^ t.

theorem ModularGroup.exists_bound_of_invariant {E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) (hf_infinity : UpperHalfPlane.IsBoundedAtImInfty f) (hf_inv : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), f (g • τ) = f τ) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C

A function on ℍ which is invariant under SL(2, ℤ), and bounded at ∞, is uniformly bounded.

theorem ModularGroup.exists_bound_of_subgroup_invariant {E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) (hf_infinity : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => f (g • τ)) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] (hf_inv : ∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C

A function on ℍ which is invariant under an arithmetic subgroup and bounded at all cusps, is uniformly bounded.

theorem ModularFormClass.exists_petersson_le {k : ℤ} (hk : 0 ≤ k) (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.IsArithmetic] {F : Type u_2} {F' : Type u_3} (f : F) (f' : F') [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] [ModularFormClass F Γ k] [ModularFormClass F' Γ k] : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

If f, f' are modular forms, then petersson k f f' is bounded by a constant multiple of max τ.im (1 / τ.im) ^ k.

theorem CuspFormClass.petersson_bounded_left (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.IsArithmetic] {F : Type u_2} {F' : Type u_3} (f : F) (f' : F') [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] [CuspFormClass F Γ k] [ModularFormClass F' Γ k] : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖ ≤ C

If f is a cusp form and f' a modular form, then petersson k f f' is bounded.

theorem CuspFormClass.petersson_bounded_right (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.IsArithmetic] {F : Type u_2} {F' : Type u_3} (f : F) (f' : F') [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] [ModularFormClass F Γ k] [CuspFormClass F' Γ k] : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖ ≤ C

If f is a modular form and f' a cusp form, then petersson k f f' is bounded.

theorem CuspFormClass.exists_bound {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (f : F) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)

A weight k cusp form is bounded in norm by a constant multiple of (im τ) ^ (-k / 2).

theorem ModularFormClass.exists_bound {k : ℤ} (hk : 0 ≤ k) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) : ∃ (C : ℝ), ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)

A weight k modular form is bounded in norm by a constant multiple of max 1 (1 / (τ.im) ^ k).

theorem qExpansion_coeff_isBigO_of_norm_isBigO {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) (e : ℝ) (hF : ⇑f =O[Filter.comap UpperHalfPlane.im (nhds 0)] fun (τ : UpperHalfPlane) => τ.im ^ (-e)) : (fun (n : ℕ) => (PowerSeries.coeff n) (ModularFormClass.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).

theorem ModularFormClass.qExpansion_isBigO {k : ℤ} (hk : 0 ≤ k) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) : (fun (n : ℕ) => (PowerSeries.coeff n) (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.

theorem CuspFormClass.qExpansion_isBigO {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F Γ k] (f : F) : (fun (n : ℕ) => (PowerSeries.coeff n) (ModularFormClass.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.