Theorems · Theorem · number theory

ModularFormClass.exists_petersson_le

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

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeFunLikeModularFormClassModularFormClass