Period pairing as a finite transversal integral in weight at least two

Proved

MTT.Cohomology.periodPairing_eq_transversal_integral_of_weight_ge_two

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

cohomologycomplex-analysismodular-forms

Let $k\ge2$ , and 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$ of weight $k$ , then

\langle f,q\rangle_{\mathrm{per}}=\sum_{\sigma\in R}\int_{\sigma\mathcal D}D(z)\,dz.

This is the finite-index unfolding formula used to pass between the quotient definition of the period pairing and translated fundamental domains. The lower bound on $k$ ensures that the symmetric-power degree $k-2$ has the intended weight.

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_of_weight_ge_two
    {N k : ℕ} (hk : 2 ≤ 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 mixed Eichler--Shimura period-pairing argument for positive level and weight at least two: contraction identities, cusp-form decay, and finite-index unfolding.

View graph