The Petersson inner product #
The Petersson inner product
$$\langle f, g \rangle = \int_D \overline{f(\tau)} \, g(\tau) \, (\operatorname{Im}\tau)^k \, d\mu(\tau)$$
of two functions on the upper half-plane, integrated over a set D — in applications a
fundamental domain — against
Mathlib's invariant measure volume : Measure ℍ (dx dy / y²,
Mathlib/Analysis/Complex/UpperHalfPlane/Measure.lean), with the integrand
petersson k f g from Mathlib/NumberTheory/ModularForms/Petersson.lean.
Main definitions #
UpperHalfPlane.peterssonInner: the set integral of the Petersson integrand over an arbitraryD : Set ℍ— a sesquilinear pairing on classes of functions whose integrands are integrable overD; positive definiteness is a separate result of the level-one-domain specialization (CuspForm.peterssonInnerFd_definite).CuspForm.peterssonInnerFd: the level-one-domain pairing of two cusp forms (over𝒟, whatever the level).CuspForm.peterssonInnerCore: for arithmetic levels, the pairing bundled as anInnerProductSpace.CoreonS_k(Γ).
Main results #
UpperHalfPlane.peterssonInner_conj_symm: Hermitian symmetry.UpperHalfPlane.petersson_smul_of_memandUpperHalfPlane.petersson_psl_smul_of_mem: the integrand is invariant underΓ, and under the image ofΓinPSL(2, ℤ)that actually acts.UpperHalfPlane.peterssonInner_eq_of_isFundamentalDomain: the pairing is the same over any two fundamental domains for that image — "the" Petersson product does not depend on the domain.UpperHalfPlane.integrableOn_petersson_fd_left: integrability of the Petersson integrand of a cusp form against a modular form over the standard fundamental domain.UpperHalfPlane.integrableOn_petersson_slash_leftandUpperHalfPlane.integrableOn_petersson_slash_right: the same for forms slashed bySL₂(ℤ)when either argument is cuspidal.UpperHalfPlane.integrableOn_petersson_sl_smul_fd_leftandUpperHalfPlane.integrableOn_petersson_sl_smul_fd_right: integrability over everySL(2, ℤ)-translate of the standard fundamental domain when either argument is cuspidal.UpperHalfPlane.integrableOn_petersson_of_measure_lt_top: integrability over any set of finite measure, for any measure, for two cusp forms of unrelated arithmetic groups. This is the shape a Hecke operator's summands present, where no single bound covers the pair.UpperHalfPlane.integrableOn_petersson_slash_left_of_measure_lt_topandUpperHalfPlane.integrableOn_petersson_slash_right_of_measure_lt_top: its specializations to one argument slashed by aGL(2, ℝ)element whose conjugate of the group is again arithmetic.UpperHalfPlane.peterssonInner_self_eq_ofReal,peterssonInner_self_re_nonneg: the self-pairing of any function is the real integral of‖h τ‖² (Im τ)^k, hence nonnegative over any domain.UpperHalfPlane.eq_zero_on_fd_of_peterssonInner_self_eq_zero: definiteness on the fundamental domain, for any continuous function with integrable self-integrand.
The pairing is parameterized by an arbitrary D : Set ℍ rather than fixing a subgroup;
for SL₂(ℤ) use D = ModularGroup.fd, and for a congruence subgroup a union of
translates of 𝒟. The topology of 𝒟/𝒟ᵒ comes from
Mathlib/NumberTheory/Modular.lean, and its measure theory (finite volume, null frontier,
𝒟-vs-𝒟ᵒ integration) from TauCeti/NumberTheory/Modular.lean.
Ported from the AINTLIB LeanModularForms project's
LeanModularForms/Modularforms/PeterssonInnerProduct.lean (Chris Birkbeck), rewritten to
consume Mathlib's MeasureSpace ℍ instance instead of constructing the hyperbolic measure.
References #
- Diamond–Shurman, A first course in modular forms, §5.4
- Miyake, Modular forms, §2.5
- The AINTLIB
LeanModularFormsproject, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms (Modularforms/PeterssonInnerProduct.lean) - AINTLIB again, at commit
6d87d596a5372d5b122c47b7082d4c3afa9b7c3b, Apache-2.0, forpeterssonInner_sum_leftandpeterssonInner_sum_right:HeckeRIngs/GL2/AdjointTheory/SummandAdjoint.lean(peterssonInner_add_left, :222;peterssonInner_T_p_family_sum_slashes_eq_aggregate_of_integrable, :620); and for the finite-measure integrability resultsintegrableOn_petersson_of_measure_lt_topand its two slash specializations:HeckeRIngs/GL2/AdjointTheory/DeltaBSystem.lean(integrableOn_petersson_cuspform_slash_glMap_of_finiteMeasure, :397).
The Petersson pairing of two functions f, g : ℍ → ℂ of weight k, integrated over
an arbitrary set D (in applications, a fundamental domain) with respect to the
invariant measure.
The integrand is conj(f(τ)) · g(τ) · (Im τ)^k, which equals
petersson k f g τ from Mathlib.NumberTheory.ModularForms.Petersson.
Equations
- UpperHalfPlane.peterssonInner k D f g = ∫ (τ : UpperHalfPlane) in D, UpperHalfPlane.petersson k f g τ
Instances For
The pairing depends on the domain only up to null sets: congruent domains give equal pairings, with no unfolding to the underlying set integral.
Over the standard fundamental domain the pairing may be computed on its interior.
The Petersson integrand is invariant under the group its arguments are modular for.
This is pointwise, and no change of variables is involved: conj (f τ) and f' τ each pick up
the automorphy factor of γ, and their product cancels against the transformation of the weight
im τ ^ k, which UpperHalfPlane.petersson_slash_SL records. So petersson k f f' is a genuine
function on the quotient Γ \ ℍ.
Not @[simp]: the left-hand side is not in simp normal form, since ModularGroup.sl_moeb
rewrites γ • τ into the GL(2, ℝ) action of γ's image. The PSL(2, ℤ) form below carries the
attribute instead, and it is the one simp can use.
The Petersson integrand is invariant under the image of Γ in PSL(2, ℤ), which is
the group that actually acts: ±I acts trivially on ℍ. This is the hypothesis
MeasureTheory.IsFundamentalDomain.setIntegral_eq asks for.
The Petersson pairing does not depend on the fundamental domain. Any two fundamental
domains for the image of Γ in PSL(2, ℤ) give the same pairing of two forms modular for Γ,
because the integrand is constant on Γ-orbits (petersson_psl_smul_of_mem).
Together with a proof that a particular set is a fundamental domain — for the union of
translates of 𝒟ᵒ that the coset sum produces, ModularGroup.isFundamentalDomain_fdo and its
subgroup form — this is what makes "the" Petersson product well defined.
Unfolding: the pairing over D is the integral of the Petersson integrand over D.
Hermitian symmetry: conj ⟨g, f⟩ = ⟨f, g⟩.
The pairing with zero on the right vanishes.
The pairing with zero on the left vanishes.
Negation in the right argument.
Negation in the left argument.
The Petersson integrand of a cusp form against a modular form is integrable over the standard fundamental domain.
The Petersson integrand of a modular form against a cusp form is integrable over the standard fundamental domain.
The Petersson self-integrand of any function is a nonnegative real:
petersson k h h τ = ‖h τ‖² (Im τ)^k.
The Petersson self-pairing of any function over any domain is the real integral of
‖h τ‖² (Im τ)^k.
The Petersson self-pairing over any domain is nonnegative, for any function:
the integrand ‖h τ‖² (Im τ)^k is.
Integrability of a one-sided slash, over any set of finite measure #
The Petersson integrand of two cusp forms for unrelated arithmetic groups is integrable over any set of finite measure.
The lemmas above need a single group: they slash both arguments by the same SL(2, ℤ) element,
so one cusp-form bound covers the pair. A Hecke operator does not do that — its summands pair
forms cuspidal for different groups, which is the situation this covers and
CuspFormClass.petersson_bounded_left does not.
The Petersson integrand of a singly slashed cusp form against a cusp form is integrable
over any set of finite measure — the orientation
peterssonInner_sum_slash_left_adjugateGL asks its caller for.
Arithmeticity of the conjugate is taken as an instance rather than derived, so that a caller with
a rational σ supplies it from Subgroup.IsArithmetic.conj and one with any other source of it
is not shut out.
The mirror of integrableOn_petersson_slash_left_of_measure_lt_top, with the second
argument slashed.
The Petersson integrand of a slashed cusp form and modular form is integrable over 𝒟:
slashing by an element of SL₂(ℤ) moves the integrand along the action, where the cusp-form
bound still applies.
The Petersson integrand of a slashed modular form and cusp form is integrable over 𝒟:
the mirror of integrableOn_petersson_slash_left, obtained from it by the conjugate symmetry
UpperHalfPlane.petersson_symm of the integrand, complex conjugation being an ℝ-linear
isometry of ℂ.
The Petersson integrand of a cusp form and a modular form is integrable over every
SL(2, ℤ)-translate of 𝒟. Transporting the integral back to 𝒟 turns the integrand into
that of the simultaneously slashed pair, where the cusp-form bound applies.
The Petersson integrand of a modular form and a cusp form is integrable over every
SL(2, ℤ)-translate of 𝒟. This is the right-cuspidal counterpart of
integrableOn_petersson_sl_smul_fd_left, obtained from it by the same conjugate symmetry of the
integrand as integrableOn_petersson_slash_right.
Additivity in the second argument.
Additivity in the first argument, given integrability of both summands.
Additivity over a finite family in the first argument. The add_left case iterated;
the hypothesis is integrability of each summand's integrand, exactly as there.
Additivity over a finite family in the second argument, the mirror of
peterssonInner_sum_left.
Scalar multiplication in the second argument.
Conjugate-scalar multiplication in the left argument.
Definiteness of the Petersson pairing on the fundamental domain: a continuous
function whose Petersson self-integrand is integrable on 𝒟 and whose self-pairing over
𝒟 vanishes is zero everywhere on 𝒟.
The nonnegative continuous integrand normSq (f τ) · (Im τ)^k is a.e. zero, hence zero on
the open domain 𝒟ᵒ, hence zero on 𝒟 = closure 𝒟ᵒ by continuity.
The level-one-domain Petersson pairing of two cusp forms: the integral over the
standard fundamental domain 𝒟 for SL₂(ℤ), whatever the level Γ — the Fd in the
name marks that the integration domain is 𝒟, not a Γ-fundamental domain.
This is not the Γ \ ℍ-normalized Petersson inner product, which integrates over a
Γ-fundamental domain. Its structure accrues by hypothesis: Hermitian symmetry and the
zero/negation laws, reality, and nonnegativity of the self-pairing are unconditional,
the scalar laws (peterssonInnerFd_smul_left/_right) require [Γ.HasDetOne], and
additivity (peterssonInnerFd_add_left/_right) and positive definiteness
(peterssonInnerFd_definite) require [Γ.IsArithmetic].
Equations
Instances For
Unfolding: the cusp-form pairing is peterssonInner over the standard domain 𝒟.
Positive definiteness from integrability, at arbitrary level: a cusp form with
integrable Petersson self-integrand over 𝒟 and vanishing self-pairing is zero.
The self-pairing vanishing forces f = 0 on the open fundamental domain 𝒟ᵒ
(eq_zero_on_fd_of_peterssonInner_self_eq_zero), and a holomorphic function on ℍ
vanishing on a nonempty open set vanishes identically
(UpperHalfPlane.eq_zero_of_frequently).
Additivity of the level-one-domain pairing in the second argument.
Additivity of the level-one-domain pairing in the first argument.
Positive definiteness of the level-one-domain pairing: a cusp form of any
arithmetic level with vanishing self-pairing is zero — the integrability hypothesis of
peterssonInnerFd_definite_of_integrable is automatic.
The self-pairing vanishes exactly on the zero form: nondegeneracy packaged with the zero law.
The 𝒟-domain Petersson pairing bundled as an InnerProductSpace.Core on
S_k(Γ) for an arithmetic level: the Hermitian interface behind Mathlib's standard
inner-product, norm, and orthogonality APIs. Evaluation is peterssonInnerCore_inner.
Deliberately not an instance: the pairing integrates over the level-one domain 𝒟, not
over a fundamental domain for Γ, so for general Γ it is not the genuine level-Γ
Petersson product, and making it canonical would silently give downstream orthogonality and
adjoint APIs the wrong domain. It is a plain def that consumers must name explicitly; 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 — it
governs unfolding during instance search and registers nothing on its own.
Equations
- CuspForm.peterssonInnerCore = { inner := CuspForm.peterssonInnerFd, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }
Instances For
Evaluation of the bundled core: its inner product is peterssonInnerFd.