Period pairing as a finite transversal integral

Open

MTT.Cohomology.periodPairing_eq_transversal_integral

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

cohomologymeasure-theorymodular-forms

Let $R$ be a finite right transversal for $\Gamma_1(N)$ in $\mathrm{SL}_2(\mathbb Z)$ . If an integrable complex density $D$ agrees on the upper half-plane with the period-contraction density attached to cusp forms $f$ and $q$ , then the period pairing is the sum of the Euclidean integrals of $D$ over the translated standard modular domains $\sigma\mathcal D$ , for $\sigma\in R$ . This packages quotient reindexing, invariance of hyperbolic measure, and the conversion $y^2\,d\mu_{\mathrm{hyp}}=dx\,dy$ .

Retired. The original statement omitted the weight-range hypothesis $2\le k$ needed for the symmetric-power degree $k-2$ and its transformation law. Use MTT.Cohomology.periodPairing_eq_transversal_integral_of_weight_ge_two instead.

Preamble

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

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

Formal statement

theorem MTT.Cohomology.periodPairing_eq_transversal_integral
    {N k : ℕ}
    (f q : CuspForm (MTT.GammaOne N) (k : ℤ))
    (R : Finset (Matrix.SpecialLinearGroup (Fin 2) ℤ))
    (hR : Subgroup.IsComplement
      (CongruenceSubgroup.Gamma1 N : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ))
      (R : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ)))
    (D : ℂ → ℂ)
    (hint : ∀ σ ∈ R, IntegrableOn D
      ((fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟) volume)
    (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 τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟, D z := by sorry

Source

Classical unfolding/change-of-variables formula for finite-index modular quotients and the invariant hyperbolic measure.

View graph