Stokes' theorem on $\Gamma\backslash\mathfrak H$ for a $\Gamma$ -invariant $(0,1)$ -form vanishing at the cusps

Proved

MTT.sum_integral_wirtinger_smul_fd_eq_zero

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

complex-analysismodular-formsnumber-theory

Let $\Gamma \le \mathrm{SL}_2(\mathbb Z)$ be a subgroup and let $R \subset \mathrm{SL}_2(\mathbb Z)$ be a finite set of representatives of the right cosets $\Gamma\backslash\mathrm{SL}_2(\mathbb Z)$ , i.e. every element of $\mathrm{SL}_2(\mathbb Z)$ is uniquely of the form $\gamma g$ with $\gamma \in \Gamma$ and $g \in R$ . With $\mathcal D = \{z : |\operatorname{Re} z| \le \tfrac12,\ |z| \ge 1\}$ the standard fundamental domain of $\mathrm{SL}_2(\mathbb Z)$ , the union $X = \bigcup_{g \in R} g\mathcal D$ is a fundamental domain for $\Gamma$ (each tile is counted twice when $-1 \notin \Gamma$ ).

Let $A : \mathfrak H \to \mathbb C$ be continuously differentiable in the real sense, and assume:

the $(0,1)$ -form $A\,d\bar z$ is $\Gamma$ -invariant, i.e. $A(\gamma z) = \overline{(cz+d)}^{\,2}\,A(z)$ for every $\gamma = \begin{pmatrix} a & b \\ c & d \end{pmatrix} \in \Gamma$ and $z \in \mathfrak H$ ;
for every $\sigma = \begin{pmatrix} a & b \\ c & d \end{pmatrix} \in \mathrm{SL}_2(\mathbb Z)$ the pulled-back coefficient $A(\sigma z)\,\overline{(cz+d)}^{-2}$ tends to $0$ as $\operatorname{Im} z \to \infty$ , uniformly in $\operatorname{Re} z$ ;
the Wirtinger derivative $\partial_z A = \tfrac12(\partial_x A - i\,\partial_y A)$ is Lebesgue integrable on each tile $g\mathcal D$ , $g \in R$ .

Then

\sum_{g \in R} \int_{g\mathcal D} \partial_z A \, dx\,dy = 0 .

Since $d(A\,d\bar z) = \partial_z A\, dz \wedge d\bar z$ , this is Stokes' theorem on the compactified quotient $\Gamma\backslash\mathfrak H$ : the boundary of $X$ consists of pairs of edges identified by elements of $\Gamma$ , whose contributions cancel by invariance, and the contributions of the horizontal caps at the cusps vanish by the decay hypothesis. The proof pulls every tile back to the standard tile, applies Green's theorem there, and cancels the side and arc terms by the permutation of $R$ induced by right multiplication with $T$ and $S$ , so that no classification of interior and exterior edges of $X$ is needed.

This is the analytic core of the Petersson-pairing (Green's identity) proof of the injectivity half of the Eichler--Shimura isomorphism (Shimura, §8.2; Columbia notes, proof of Theorem 1): for $A = \langle \Phi,\ \overline{f}\,(\bar z X + Y)^{k-2}\rangle$ with $\Phi$ a $\Gamma$ -invariant (mixed) Eichler integral and $f$ a cusp form, $\partial_z A$ is a constant multiple of the Petersson integrand $\overline{f}\,g\,y^{k-2}$ , and the vanishing of $\sum_g \int_{g\mathcal D}\partial_z A$ for all $f$ forces $g = 0$ .

Formalization note. $\mathcal D$ is Mathlib's ModularGroup.fd; the tile $g\mathcal D$ is the image of 𝒟 under the Möbius action of $g$ on $\mathfrak H$ , viewed in $\mathbb C$ ; integrals are Lebesgue integrals on $\mathbb C$ ; Subgroup.IsComplement encodes the right-coset representatives; denom γ τ = cτ + d; the Wirtinger derivative is written through the real Fréchet derivative fderiv ℝ A z; the decay in (2) is IsZeroAtImInfty of the pulled-back coefficient.

Preamble

import Mathlib.NumberTheory.ModularForms.Bounds
set_option autoImplicit false
noncomputable section
open UpperHalfPlane MeasureTheory
open scoped MatrixGroups Modular

Formal statement

theorem MTT.sum_integral_wirtinger_smul_fd_eq_zero
    {Γ : Subgroup SL(2, ℤ)} {R : Finset SL(2, ℤ)}
    (hR : Subgroup.IsComplement (Γ : Set SL(2, ℤ)) (R : Set SL(2, ℤ)))
    {A : ℂ → ℂ} (hA : ContDiffOn ℝ 1 A upperHalfPlaneSet)
    (hinv : ∀ γ ∈ Γ, ∀ τ : ℍ, A ((γ • τ : ℍ) : ℂ) = (starRingEnd ℂ (denom γ τ)) ^ 2 * A τ)
    (hdecay : ∀ g : SL(2, ℤ), IsZeroAtImInfty
      fun τ : ℍ ↦ A ((g • τ : ℍ) : ℂ) * ((starRingEnd ℂ (denom g τ)) ^ 2)⁻¹)
    (hint : ∀ g ∈ R, IntegrableOn
      (fun z ↦ (1 / 2 : ℂ) * (fderiv ℝ A z 1 - Complex.I * fderiv ℝ A z Complex.I))
      ((fun τ : ℍ ↦ ((g • τ : ℍ) : ℂ)) '' 𝒟) volume) :
    ∑ g ∈ R, ∫ z in (fun τ : ℍ ↦ ((g • τ : ℍ) : ℂ)) '' 𝒟,
      (1 / 2 : ℂ) * (fderiv ℝ A z 1 - Complex.I * fderiv ℝ A z Complex.I) = 0 := by sorry

Source

G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions (1971), §8.2, the Stokes/Green identity on a fundamental domain, (8.2.17)–(8.2.22), pp. 223–226; Columbia Spring 2021 modular-forms seminar notes, Week 4–5, §1.2, proof of Theorem 1, p. 9 (∫_{∂X} F ∧ ω(g) = Σ_i (∫_{α_i s_i} − ∫_{s_i}) F ∧ ω(g) = 0 for a fundamental domain X with paired boundary edges), https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf. The statement isolates the Stokes/edge-cancellation step for a general Γ-invariant (0,1)-form; the tile-by-tile assembly with right-coset permutation is a reorganisation of the same boundary cancellation.

View graph

Stokes' theorem on Γ\H\Gamma\backslash\mathfrak HΓ\H for a Γ\GammaΓ-invariant (0,1)(0,1)(0,1)-form vanishing at the cusps

Stokes' theorem on $\Gamma\backslash\mathfrak H$ for a $\Gamma$ -invariant $(0,1)$ -form vanishing at the cusps