Period pairing as Euclidean integrals over arbitrary coset tiles

Proved

MTT.Cohomology.periodPairing_eq_sum_tiles

by cbirkbeck · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

measure-theorymodular-formsperiods

Let $f,q\in S_k(\Gamma_1(N))$ with $k\ge2$ , and let $R$ be a finite set of representatives for the right cosets $\Gamma_1(N)\backslash\mathrm{SL}_2(\mathbb Z)$ . Let $D:\mathbb C\to\mathbb C$ agree on the upper half-plane with the determinant-contraction density

D(z)=B_{k-2}\bigl(f(z)(zX+Y)^{k-2},\overline{q(z)}(\bar zX+Y)^{k-2}\bigr).

For the standard modular domain $\mathcal D$ , the period pairing is

\mathcal B_{k-2}(f,q)=\sum_{\sigma\in R}\int_{\sigma\mathcal D}D(z)\,dx\,dy.

The left side uses hyperbolic measure and the fixed quotient representatives in the definition of the period pairing; the right side uses Euclidean area and the arbitrary representatives $R$ . The equality retains the same central multiplicity on both sides. This is the change-of-measure interface needed to apply Stokes' theorem to the MTT period pairing.

Preamble

import Definitions.Def_MTT_PeriodPairing
import Mathlib.NumberTheory.ModularForms.Bounds
import Mathlib.GroupTheory.Complement

set_option autoImplicit false
noncomputable section
open UpperHalfPlane MeasureTheory
open scoped MatrixGroups Modular ComplexConjugate
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.periodPairing_eq_sum_tiles {N k : ℕ} (hk : 2 ≤ k)
    (f q : CuspForm (MTT.GammaOne N) (k : ℤ))
    (R : Finset SL(2, ℤ))
    (hR : Subgroup.IsComplement (CongruenceSubgroup.Gamma1 N : Set SL(2, ℤ))
      (R : Set SL(2, ℤ)))
    (D : ℂ → ℂ)
    (hD : ∀ z : ℍ, D z = periodContraction (k - 2)
      (f z • periodPower (k - 2) z)
      (conj (q z) • periodPower (k - 2) (conj (z : ℂ)))) :
    periodPairing N (k - 2) f q =
      ∑ σ ∈ R, ∫ z in (fun τ : ℍ => ((σ • τ : ℍ) : ℂ)) '' ModularGroup.fd,
        D z := by sorry

Source

Columbia Spring 2021 modular-forms seminar notes, Week 4–5, §1.2, pp. 8–10, proof of Theorem 1, especially the invariant quotient pairing on p. 9; https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. This is the explicit finite-coset/change-of-measure identity underlying that quotient integral, with the source hypothesis k >= 2 retained. The contraction calculation is adapted from accepted Prove2Me proof 777707bf-f8aa-4fd9-8d82-71afe645b027, Part A, by cbirkbeck.

View graph