Integrability of period-contraction densities on modular tiles

Proved

MTT.Cohomology.periodDensity_integrableOn_tile

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

measure-theorymodular-formsperiods

Let $N>0$ , $k\ge2$ , and $f,q\in S_k(\Gamma_1(N))$ . Suppose $D:\mathbb C\to\mathbb C$ agrees on the upper half-plane with

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

Then $D$ is Lebesgue integrable over $\sigma\mathcal D$ for every $\sigma\in\mathrm{SL}_2(\mathbb Z)$ , where $\mathcal D$ is the standard modular fundamental domain. Values of $D$ outside the upper half-plane are irrelevant. This supplies the integrability input for applying the Wirtinger integral identity to period pairings.

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.periodDensity_integrableOn_tile {N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k)
    (f q : CuspForm (MTT.GammaOne N) (k : ℤ)) (σ : SL(2, ℤ))
    (D : ℂ → ℂ)
    (hD : ∀ z : ℍ, D z = periodContraction (k - 2)
      (f z • periodPower (k - 2) z)
      (conj (q z) • periodPower (k - 2) (conj (z : ℂ)))) :
    IntegrableOn D ((fun z : ℍ => ((σ • z : ℍ) : ℂ)) '' ModularGroup.fd) := by sorry

Source

Columbia Spring 2021 modular-forms seminar notes, Week 4–5, §1.2, pp. 8–10, Theorem 1 and its period pairing; https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. The standard finite-hyperbolic-area and Petersson-bound argument is adapted from AINTLIB, projects/LeanModularForms/LeanModularForms/Modularforms/PeterssonInnerProduct.lean, hyperbolicMeasure_fd_lt_top and peterssonInner_integrableOn, commit eb9621e7bcb0ce220ad53983ec45d987cb5b9002 (Chris Birkbeck, Apache 2.0). The coefficient identities are adapted from cbirkbeck's accepted Prove2Me proof 777707bf-f8aa-4fd9-8d82-71afe645b027, Part A. Positive level and weight at least two are retained explicitly.

View graph