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 last 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.

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, via MeasureTheory.setIntegral_congr_set).
• ModularGroup.sl_smul_set: the SL(2, ℤ)-action on subsets of ℍ is the GL(2, ℝ)-action along the coercion.
• ModularGroup.isOpen_smul_fdo and ModularGroup.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.

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).

The final section on translates of 𝒟ᵒ was developed in Tau Ceti and has no counterpart in that AINTLIB source.

theorem ModularGroup.volume_fd_lt_top : MeasureTheory.volume fd < ⊤

The invariant measure of the standard fundamental domain is finite.

theorem ModularGroup.volume_frontier_fd : MeasureTheory.volume (frontier fd) = 0

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 ℂ.

theorem ModularGroup.fd_ae_eq_fdo : fd =ᵐ[MeasureTheory.volume] fdo

fd and fdo are a.e. equal w.r.t. the invariant measure.

Disjointness of translates of the open fundamental domain

@[simp]

theorem ModularGroup.sl_smul_set (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (S : Set UpperHalfPlane) : γ • S = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) • S

The SL(2, ℤ)-action on subsets of ℍ is the GL(2, ℝ)-action along the coercion, the pointwise-image counterpart of ModularGroup.sl_moeb. This is useful as a rewrite even though the two actions are definitionally equal.

theorem ModularGroup.isOpen_smul_fdo (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : IsOpen (γ • fdo)

Every translate of the open fundamental domain is open: translation is a homeomorphism of ℍ.

theorem ModularGroup.disjoint_smul_fdo {γ δ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (h₁ : γ⁻¹ * δ ≠ 1) (h₂ : γ⁻¹ * δ ≠ -1) : Disjoint (γ • fdo) (δ • fdo)

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.