The Petersson inner product for a finite-index subgroup #
The Petersson pairing of Mathlib.NumberTheory.ModularForms.Petersson is integrated over
the standard fundamental domain 𝒟 of SL₂(ℤ), which is too small for forms on a proper
subgroup Γ ≤ SL₂(ℤ): a fundamental domain for Γ is tiled by [SL₂(ℤ) : Γ·{±I}] translates of
𝒟. This file defines the pairing on S_k(Γ) as the corresponding sum over cosets,
⟪f, g⟫ = ∑_{[δ] ∈ SL₂(ℤ)/Γ·{±I}} ∫_𝒟 conj((f ∣[k] δ⁻¹)(τ)) (g ∣[k] δ⁻¹)(τ) (Im τ)^k dμ,
and establishes that it is a positive-definite Hermitian form: conjugate-symmetric, additive
and complex-linear in the second argument, conjugate-linear in the first, and vanishing on
the diagonal only at 0.
The sum runs over the cosets of Γ·{±I}, not of Γ: since -I acts trivially on ℍ, the
cosets of q and -q carry the same translate of 𝒟, so indexing by Γ alone would count
every translate twice whenever -I ∉ Γ. The summand does not depend on the chosen
representative: the Γ part of the subgroup fixes a Γ-invariant form, and -I scales it by
the real sign (-1)^k, which the conjugate-linear pairing cancels against itself.
Finite index is what makes the sum finite, and it is also exactly what makes the image of Γ
in GL(2, ℝ) arithmetic, which the definiteness argument needs. Taking Γ = Γ₁(N) gives the
classical level-N Petersson product.
The pairing is deliberately left un-normalized by the volume of the fundamental domain: a positive-definite Hermitian form is all that the adjoint theory downstream needs.
Main definitions #
CuspForm.peterssonInnerCosets: the Petersson inner product onS_k(Γ).
Main results #
CuspForm.exists_slash_eq_smul_of_mem_withCenter: slashing by an element ofΓ·{±I}scales every form by one and the same unimodular constant.CuspForm.peterssonInner_slash_of_mem_withCenter: the summand is independent of the coset representative, which is what makes the sum well defined.CuspForm.peterssonInner_slash_inv_out: the same, for the chosen representative of the coset of an arbitraryδ, the form in which the sum is reindexed.CuspForm.peterssonInnerCosets_conj_symm: Hermitian symmetry.CuspForm.peterssonInnerCosets_add_left/_right,_smul_right,_smul_left: sesquilinearity.CuspForm.peterssonInnerCosets_definite: positive definiteness.CuspForm.peterssonInnerCosets_ofLe_ofLe: restricting two forms forΓto a finite-indexΓ' ≤ Γmultiplies their pairing by the index[Γ·{±I} : Γ'·{±I}].CuspForm.peterssonInnerCosetsCore: the pairing bundled as anInnerProductSpace.Core.
Ported from the AINTLIB LeanModularForms project
(LeanModularForms/Modularforms/PeterssonLevelN.lean, Chris Birkbeck,
https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), with the
bespoke hyperbolic measure replaced by the volume of ℍ used throughout TauCeti, and
stated for an arbitrary finite-index subgroup rather than only Γ₁(N).
References #
The coset space of Γ.withCenter is finite when Γ has finite index; this is what makes
the defining sum of CuspForm.peterssonInnerCosets a finite one.
The Petersson inner product on S_k(Γ) for a finite-index Γ ≤ SL₂(ℤ): the sum,
over the cosets of Γ·{±I} in SL₂(ℤ), of the level-one pairing of the correspondingly
slashed forms. The subgroup is Γ.withCenter, not Γ, because -I acts trivially on ℍ.
For Γ = Γ₁(N) this is the classical level-N Petersson product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unfolding: the pairing is the coset sum of level-one pairings.
Hermitian symmetry of the coset pairing.
The coset pairing vanishes when its second argument does.
The coset pairing vanishes when its first argument does.
Slashing by Γ·{±I} scales every form by one and the same unimodular constant: by 1
on Γ itself, where the forms are invariant, and by (-1)^k on its negatives, since -I acts
trivially on ℍ and contributes only the automorphy factor. Unimodularity conj c * c = 1 is
what makes the constant invisible to the conjugate-linear Petersson pairing.
Slashing both arguments by an element of Γ·{±I} is invisible to the level-one-domain
pairing, before any common further slash β.
This is the general form of peterssonInner_slash_of_mem_withCenter below, which is the β = 1
case. It is what the coset-representative arguments consume: the pairing of two forms slashed into
a coset does not depend on which representative of that coset is used to reach it, so the defining
sum of the Petersson product may be reindexed over the coset space.
The summand does not depend on the coset representative: the level-one-domain pairing
is unchanged by slashing with Γ·{±I}. This is what lets the defining sum be reindexed over the
coset space. It is the β = 1 case of peterssonInner_slash_slash_of_mem_withCenter.
The summand of the Petersson product is a function of the coset. Replacing the chosen
representative q.out of a coset by any other element of it does not change the level-one-domain
pairing of the correspondingly slashed forms. This is the form in which the defining sum of
peterssonInnerCosets is reindexed along a bijection onto the coset space.
Positive definiteness of the Petersson inner product: every summand of the self-pairing is non-negative, so the whole sum vanishes only if the identity-coset summand does, and that summand is the level-one pairing.
Negation in the second argument.
Negation in the first argument.
Additivity in the second argument.
Complex-linearity in the second argument.
Conjugate-linearity in the first argument.
Additivity in the first argument.
The self-pairing is nonnegative: each coset summand is a nonnegative real.
The self-pairing is real: its imaginary part vanishes, by Hermitian symmetry.
The self-pairing vanishes exactly on the zero form.
Restriction to a sublevel #
Restriction to a sublevel multiplies the Petersson product by the index. For subgroups
Γ' ≤ Γ of finite index in SL₂(ℤ) and cusp forms f, g for Γ, read as cusp forms for
Γ',
⟪f, g⟫_Γ' = [Γ·{±I} : Γ'·{±I}] · ⟪f, g⟫_Γ.
The Petersson pairing bundled as an InnerProductSpace.Core on S_k(Γ): the Hermitian
interface behind Mathlib's inner-product, norm, orthogonality and adjoint APIs, which the
adjoint theory consumes. Evaluation is peterssonInnerCosetsCore_inner.
Unlike the level-one peterssonInnerCore, this one does integrate over a fundamental domain
for the group in question, so it is the genuine Petersson product of Γ. It is still a
plain def rather than an instance, following the same convention: consumers name it
explicitly, and no InnerProductSpace instance is derived from it. The
@[instance_reducible] attribute is required by Lean's class-definition reducibility linter
for any def of class type.
Equations
- CuspForm.peterssonInnerCosetsCore = { inner := CuspForm.peterssonInnerCosets, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }
Instances For
Evaluation of the bundled core: its inner product is peterssonInnerCosets.