Theorems · Theorem · number theory

CuspFormClass.petersson_bounded_right

∀ (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]
  [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.

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

0 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeFunLikeModularFormClassCuspFormClass