Theorems · Theorem · number theory

UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left

∀ {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},
  UpperHalfPlane.IsZeroAtImInfty ⇑f →
    ∀ (f' : 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

2 results in Mathlib

Foundations

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

Assumes

FunLikeFunLikeFactSubgroup.HasDetPlusMinusOneDiscreteTopologyModularFormClassModularFormClass