Period pairings as finite sums of Wirtinger integrals

Open

MTT.Cohomology.period_pairings_eq_wirtinger_sums

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

measure-theorymodular-formsperiods

Let $R$ be a finite set of right-coset representatives for $\Gamma_1(N)$ in $\mathrm{SL}_2(\mathbb Z)$ . Suppose two scalar functions $A_1,A_2$ have integrable Wirtinger derivatives on every translated standard domain and satisfy

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

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

Then the corresponding period pairings are exactly

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

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

This is the change-of-domain and change-of-measure interface between the quotient-based definition of the period pairing and finite sums of Euclidean integrals on fundamental-domain tiles.

Retired. The original statement omitted the necessary weight-range hypothesis $2\le k$ . Use MTT.Cohomology.period_pairings_eq_wirtinger_sums_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.period_pairings_eq_wirtinger_sums
    {N k : ℕ}
    (g v 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) ℤ)))
    {A₁ A₂ : ℂ → ℂ}
    (hint₁ : ∀ σ ∈ R, IntegrableOn
      (fun z ↦ (1 / 2 : ℂ) *
        (fderiv ℝ A₁ z 1 - Complex.I * fderiv ℝ A₁ z Complex.I))
      ((fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟) volume)
    (hint₂ : ∀ σ ∈ R, IntegrableOn
      (fun z ↦ (1 / 2 : ℂ) *
        (fderiv ℝ A₂ z 1 - Complex.I * fderiv ℝ A₂ z Complex.I))
      ((fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟) volume)
    (hderiv₁ : ∀ z : ℍ,
      (1 / 2 : ℂ) *
          (fderiv ℝ A₁ z 1 - Complex.I * fderiv ℝ A₁ z Complex.I) =
        periodContraction (k - 2)
          (g z • periodPower (k - 2) (z : ℂ))
          (conj (q z) • periodPower (k - 2) (conj (z : ℂ))))
    (hderiv₂ : ∀ z : ℍ,
      (1 / 2 : ℂ) *
          (fderiv ℝ A₂ z 1 - Complex.I * fderiv ℝ A₂ z Complex.I) =
        -conj (periodContraction (k - 2)
          (q z • periodPower (k - 2) (z : ℂ))
          (conj (v z) • periodPower (k - 2) (conj (z : ℂ))))) :
    periodPairing N (k - 2) g q =
        ∑ σ ∈ R, ∫ z in (fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟,
          (1 / 2 : ℂ) *
            (fderiv ℝ A₁ z 1 - Complex.I * fderiv ℝ A₁ z Complex.I) ∧
    periodPairing N (k - 2) q v =
        -conj (∑ σ ∈ R, ∫ z in (fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟,
          (1 / 2 : ℂ) *
            (fderiv ℝ A₂ z 1 - Complex.I * fderiv ℝ A₂ z Complex.I)) := by sorry

Source

Columbia Spring 2021 modular-forms seminar notes, Week 4–5, §1.2, proof of Theorem 1, pp. 7–10, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf; change of variables from hyperbolic measure to Euclidean area on a finite coset fundamental domain.

View graph