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
Instances For
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)
:
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 ∈ Γ)
: