Theorems · Theorem · number theory

CuspFormClass.petersson_bounded_left

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

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

2 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeFunLikeCuspFormClassModularFormClass