The Petersson product of conjugate forms

The conjugate form f_ρ(τ) = conj (f (-conj τ)) is the slash of f by the reflection J = !![-1, 0; 0, 1] (CuspForm.conj). The reflection τ ↦ -conj τ preserves the invariant measure of ℍ, and the Petersson integrand of f ∣[k] J and g ∣[k] J at τ is the complex conjugate of that of f and g at J • τ. So conjugating both arguments conjugates the Petersson product,

⟪f_ρ, g_ρ⟫ = conj ⟪f, g⟫,

for a finite-index Γ ≤ SL₂(ℤ) normalized by J, such as Γ₀(N) and Γ₁(N): J carries a fundamental domain of Γ to another one. In particular f ↦ f_ρ preserves Petersson orthogonality, which is how it acts on the old and new subspaces.

Main results

• UpperHalfPlane.peterssonInner_slash_slash_J: slashing both arguments by J conjugates the pairing and reflects its domain.
• CuspForm.peterssonInnerCosets_conj_conj: ⟪f_ρ, g_ρ⟫ = conj ⟪f, g⟫ on S_k(Γ).

References

• T. Miyake, Modular forms, §4.6, where the conjugate form is written f_ρ.

theorem UpperHalfPlane.peterssonInner_slash_slash_J (k : ℤ) (S : Set UpperHalfPlane) (f h : UpperHalfPlane → ℂ) : peterssonInner k S (SlashAction.map k J f) (SlashAction.map k J h) = (starRingEnd ℂ) (peterssonInner k (J • S) f h)

Slashing both arguments by the reflection J conjugates the Petersson pairing: ⟪f ∣[k] J, h ∣[k] J⟫_S = conj ⟪f, h⟫_{J • S}. The slash by the determinant -1 matrix J conjugates values, and J preserves the invariant measure.

theorem CuspForm.peterssonInnerCosets_conj_conj {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (hJ : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ ≤ ConjAct.toConjAct UpperHalfPlane.J⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : (conj hJ f).peterssonInnerCosets (conj hJ g) = (starRingEnd ℂ) (f.peterssonInnerCosets g)

Conjugating both forms conjugates the Petersson product: ⟪f_ρ, g_ρ⟫ = conj ⟪f, g⟫ on S_k(Γ), for a finite-index Γ ≤ SL₂(ℤ) normalized by the reflection J.