Theorems · Theorem · number theory

ModularFormClass.exists_bound

∀ {k : ℤ},
  0 ≤ k →
    ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {F : Type u_2} [inst : 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).

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeModularFormClass