The Petersson scalar product

For f, f' functions ℍ → ℂ, we define petersson k f f' to be the function τ ↦ conj (f τ) * f' τ * τ.im ^ k.

We show this function is (weight 0) invariant under Γ if f, f' are (weight k) invariant under Γ.

noncomputable def UpperHalfPlane.petersson (k : ℤ) (f f' : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : ℂ

The integrand in the Petersson scalar product of two modular forms.

Equations

• UpperHalfPlane.petersson k f f' τ = (starRingEnd ℂ) (f τ) * f' τ * ↑τ.im ^ k

theorem UpperHalfPlane.petersson_continuous (k : ℤ) {f f' : UpperHalfPlane → ℂ} (hf : Continuous f) (hf' : Continuous f') : Continuous (petersson k f f')

theorem UpperHalfPlane.petersson_slash (k : ℤ) (f f' : UpperHalfPlane → ℂ) (g : GL (Fin 2) ℝ) (τ : UpperHalfPlane) : petersson k (SlashAction.map k g f) (SlashAction.map k g f') τ = ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 2) * (σ g) (petersson k f f' (g • τ))

theorem UpperHalfPlane.petersson_slash_SL (k : ℤ) (f f' : UpperHalfPlane → ℂ) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : petersson k (SlashAction.map k g f) (SlashAction.map k g f') τ = petersson k f f' (g • τ)

theorem UpperHalfPlane.petersson_symm (k : ℤ) (f f' : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : petersson k f' f τ = (starRingEnd ℂ) (petersson k f f' τ)

theorem UpperHalfPlane.petersson_norm_symm (k : ℤ) (f f' : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : ‖petersson k f' f τ‖ = ‖petersson k f f' τ‖

theorem SlashInvariantFormClass.norm_petersson_smul {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] {k : ℤ} {g : GL (Fin 2) ℝ} {τ : UpperHalfPlane} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] [SlashInvariantFormClass F Γ k] {f : F} [SlashInvariantFormClass F' Γ k] {f' : F'} (hg : g ∈ Γ) : ‖UpperHalfPlane.petersson k (⇑f) (⇑f') (g • τ)‖ = ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖

theorem SlashInvariantFormClass.petersson_smul {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] {k : ℤ} {g : GL (Fin 2) ℝ} {τ : UpperHalfPlane} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [SlashInvariantFormClass F Γ k] {f : F} [SlashInvariantFormClass F' Γ k] {f' : F'} (hg : g ∈ Γ) : UpperHalfPlane.petersson k (⇑f) (⇑f') (g • τ) = UpperHalfPlane.petersson k (⇑f) (⇑f') τ

theorem UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [ModularFormClass F Γ k] [ModularFormClass F' Γ k] {f : F} (h_bd : IsZeroAtImInfty ⇑f) (f' : F') : ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun (τ : UpperHalfPlane) => 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.

theorem UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [ModularFormClass F Γ k] [ModularFormClass F' Γ k] (f : F) {f' : F'} (h_bd : IsZeroAtImInfty ⇑f') : ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun (τ : UpperHalfPlane) => 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.

theorem UpperHalfPlane.IsZeroAtImInfty.of_exp_decay {E : Type u_3} [NormedAddCommGroup E] {f : UpperHalfPlane → E} (hf : ∃ c > 0, f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)) : IsZeroAtImInfty f

theorem UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [ModularFormClass F Γ k] [ModularFormClass F' Γ k] {f : F} (h_bd : IsZeroAtImInfty ⇑f) (f' : F') : IsZeroAtImInfty (petersson k ⇑f ⇑f')

theorem UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_right {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [FunLike F' UpperHalfPlane ℂ] (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [ModularFormClass F Γ k] [ModularFormClass F' Γ k] (f : F) {f' : F'} (h_bd : IsZeroAtImInfty ⇑f') : IsZeroAtImInfty (petersson k ⇑f ⇑f')