Measure theory of the standard fundamental domain #
The measure theory of the standard fundamental domain 𝒟 = ModularGroup.fd for SL₂(ℤ),
complementing its topology from Mathlib/NumberTheory/Modular.lean: 𝒟 has finite
invariant measure, its frontier is null, and therefore integrals over 𝒟 and its interior
𝒟ᵒ agree. The next section records that the translates γ • 𝒟ᵒ are open and that two are
disjoint unless their translating elements differ by a sign; these facts turn suitable finite
sums of integrals over translates into a single integral over their union.
Those two halves are exactly what MeasureTheory.IsFundamentalDomain asks for, and the last
section assembles them: 𝒟ᵒ is a fundamental domain in the measure-theoretic sense. The group
acting has to be PSL(2, ℤ), not SL(2, ℤ) — −I fixes every point of ℍ, so the translates
indexed by SL(2, ℤ) are never pairwise disjoint — and the domain has to be the open 𝒟ᵒ, on
which Mathlib's Second Fundamental Domain Lemma is an honest disjointness rather than a
statement about a boundary. Covering is then only almost everywhere, the two domains differing
by the null frontier. Tiled over the cosets of a subgroup this gives a fundamental domain at
every level, which is what a Petersson product for a congruence subgroup is an integral over.
Main results #
ModularGroup.volume_fd_lt_top: the standard fundamental domain has finite invariant measure.ModularGroup.volume_frontier_fd: the frontier of𝒟has zero invariant measure.ModularGroup.fd_ae_eq_fdo:𝒟and𝒟ᵒagree almost everywhere (so set integrals over them coincide, viaMeasureTheory.setIntegral_congr_set).ModularGroup.isOpen_smul_fdoandModularGroup.disjoint_smul_fdo: the translates of the open fundamental domain are open, and two of them are disjoint unless the translating elements differ by a sign.ModularGroup.isFundamentalDomain_fdo:𝒟ᵒis a fundamental domain forPSL(2, ℤ)acting onℍwith the invariant measure.ModularGroup.isFundamentalDomain_iUnion_out_inv_smul_fdo: the coset tiling of𝒟ᵒis a fundamental domain for any subgroup ofPSL(2, ℤ).ModularGroup.isFundamentalDomain_iUnion_out_inv_smul_fdo_withCenter: the same tiling indexed bySL(2, ℤ) ⧸ Γ.withCenter, which is the indexing the Petersson product uses.ModularGroup.isFundamentalDomain_smul_of_inv_conjAct_eq: an element ofGL(2, ℝ)conjugating the image ofΓonto that ofΓ'carries a fundamental domain forΓto one forΓ'— the step that lets a Petersson product be compared with its translate under the Fricke or an Atkin–Lehner matrix, or under the matrix of a double coset operator.
Split out of the Petersson inner-product development ported from the AINTLIB
LeanModularForms project
(https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms,
Modularforms/PeterssonInnerProduct.lean, Chris Birkbeck).
Two of the results correspond to statements in that project:
ModularGroup.isFundamentalDomain_fdo to isFundamentalDomain_fdo_PSL
(Modularforms/PSL2Action.lean), and ModularGroup.isFundamentalDomain_iUnion_out_inv_smul_fdo
to isFundamentalDomain_Gamma1_PSL (Modularforms/PeterssonLevelN.lean), of which it is the
arbitrary-subgroup form — that one states the tiling for the image of Γ₁(N). Both are stated
here for Mathlib's volume : Measure ℍ rather than that project's own hyperbolic measure. The
results on translates of 𝒟ᵒ have no counterpart there.
The invariant measure of the standard fundamental domain is finite.
The frontier of the standard fundamental domain has zero invariant measure.
frontier 𝒟 = 𝒟 \ 𝒟ᵒ ⊆ {normSq = 1} ∪ {Re = 1/2} ∪ {Re = −1/2}, each of which has
zero Lebesgue measure in ℂ.
fd and fdo are a.e. equal w.r.t. the invariant measure.
Disjointness of translates of the open fundamental domain #
Every translate of the open fundamental domain is open: translation is a homeomorphism
of ℍ.
Distinct translates of the open fundamental domain are disjoint. A point of
γ • 𝒟ᵒ ∩ δ • 𝒟ᵒ exhibits two points of 𝒟ᵒ in the same SL(2, ℤ)-orbit, which forces
γ⁻¹δ = ±I by ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fdo. Both signs must be excluded,
−I acting trivially on ℍ: it is the translates indexed by SL(2, ℤ)/{±I}, not by
SL(2, ℤ), that are genuinely distinct.
𝒟ᵒ is a fundamental domain for PSL(2, ℤ) #
The open standard domain 𝒟ᵒ is a fundamental domain for PSL(2, ℤ) acting on ℍ,
with respect to the invariant measure: almost every point of ℍ is carried into 𝒟ᵒ by some
element, and distinct elements carry 𝒟ᵒ to sets meeting in a null set.
It is PSL(2, ℤ) and the open domain, not SL(2, ℤ) and 𝒟, that make the statement true;
the module docstring says why.
A fundamental domain for a subgroup of PSL(2, ℤ): the union of the [PSL(2, ℤ) : H]
translates (q.out)⁻¹ • 𝒟ᵒ, one for each coset q ∈ PSL(2, ℤ) ⧸ H, is a fundamental domain for
H acting on ℍ with the invariant measure — for every subgroup, no finiteness needed, since
PSL(2, ℤ) is countable and so is each of its coset spaces. At a congruence subgroup this is the
domain a Petersson product at level N is an integral over.
The same tiling, indexed by the cosets of Γ·{±I} in SL(2, ℤ). For
Γ ≤ SL(2, ℤ), the translates (q.out)⁻¹ • 𝒟ᵒ taken over q ∈ SL(2, ℤ) ⧸ Γ.withCenter tile a
fundamental domain for the image of Γ in PSL(2, ℤ).
This is the shape the Petersson product presents: CuspForm.peterssonInnerCosets sums over
SL(2, ℤ) ⧸ Γ.withCenter, one coset at a time, because ±I acts trivially on ℍ. The
PSL(2, ℤ)-indexed statement above does not apply to it directly: the two index sets are
different types, and Quotient.out picks unrelated representatives in each, so the two unions
are different sets.
A conjugating translate of a fundamental domain is a fundamental domain for the conjugate
group. If α ∈ GL(2, ℝ) conjugates the image of Γ in GL(2, ℝ) onto that of Γ' —
α⁻¹ Γ' α = Γ, stated as ConjAct.toConjAct α⁻¹ • Γ' = Γ — then for every fundamental domain
S of the image of Γ in PSL(2, ℤ), the translate α • S is a fundamental domain for the
image of Γ': α carries Γ-orbits on ℍ to Γ'-orbits, since α γ α⁻¹ acts on ℍ as an
element of Γ' does, and it preserves the invariant measure.
α need not lie in SL(2, ℤ), nor even have integral entries. With Γ' = Γ this is the case of
a normaliser: the Fricke matrix !![0, -1; N, 0], which normalises Γ₁(N) and Γ₀(N), and the
Atkin–Lehner matrices, which normalise Γ₀(N). With Γ' ≠ Γ it is the case of the double coset
operators, where a rational α carries Γ ∩ α⁻¹ Γ α onto α Γ α⁻¹ ∩ Γ. That is also why
MeasureTheory.IsFundamentalDomain.smul_of_eq_conjAct_pointwise_smul does not apply: it translates
by an element of the acting group itself, and α does not lie in PSL(2, ℤ).