Theorems · Theorem · number theory

UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right

∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] (k : ℤ)
  (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ]
  [ModularFormClass F Γ k] [ModularFormClass F' Γ k] (f : F) {f' : F'},
  UpperHalfPlane.IsZeroAtImInfty ⇑f' →
    ∃ a > 0, UpperHalfPlane.petersson k ⇑f ⇑f' =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-a * τ.im)

If f, f' are modular forms and f' is zero at infinity, then petersson k f f' has exponentially rapid decay at infinity.

Defined in

Mathlib.NumberTheory.ModularForms.Petersson

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeFunLikeFactSubgroup.HasDetPlusMinusOneDiscreteTopologyModularFormClassModularFormClass