Green's theorem on the truncated standard fundamental-domain tile

Proved

MTT.GreenTile.green_tile_truncated_fd

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

complex-analysisfundamental-domainintegrationmodular-forms

Let $H>1$ and let $T_H=\{(x,y)\in\mathbf R^2:\ |x|<\tfrac12,\ \sqrt{1-x^2}<y<H\}$ be the standard fundamental domain of $SL_2(\mathbf Z)$ truncated at height $H$ : the region between the unit-circle arc $\varphi(x)=\sqrt{1-x^2}$ and the horizontal line $y=H$ over $|x|<\tfrac12$ . Let $A,B:\mathbf R^2\to\mathbf C$ be continuous on the open set $V=\{|x|<1,\ y>0\}\supset\overline{T_H}$ , with $A$ differentiable in $x$ and $B$ differentiable in $y$ there, and with continuous partial derivatives $\partial_xA$ , $\partial_yB$ on $V$ . Then (Green's theorem, in divergence form, for the tile)

\iint_{T_H}\big(\partial_xA+\partial_yB\big)\,dx\,dy=\int_{-1/2}^{1/2}\big[B(x,H)-B(x,\varphi(x))\big]\,dx+\int_{-1/2}^{1/2}A(x,\varphi(x))\,\varphi'(x)\,dx+\int_{\sqrt3/2}^{H}\big[A(\tfrac12,y)-A(-\tfrac12,y)\big]\,dy,

where $\varphi'(x)=-x/\sqrt{1-x^2}$ . The right-hand side is the counterclockwise boundary integral $\oint_{\partial T_H}(A\,dy-B\,dx)$ over the four boundary pieces (the arc, the right edge $x=\tfrac12$ , the top $y=H$ , the left edge $x=-\tfrac12$ ), and the arc contributes only through the term $\int A(x,\varphi(x))\varphi'(x)\,dx$ since $dy=\varphi'(x)\,dx$ there.

This is the region-Stokes step needed to turn the Petersson area integral over a fundamental domain into a boundary integral (Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, (8.2.17)–(8.2.22)); Mathlib's divergence theorem is available only for rectangles, and the standard tile has a curvilinear side. Fundamental domains of $\Gamma_1(N)$ are finite unions of $SL_2(\mathbf Z)$ -translates of this tile, so the identity, applied tile by tile after pulling back by the translating matrices, is the analytic input for the Eichler–Shimura pairing identity used in the injectivity half of Eichler–Shimura.

Formalization Note The area integral is over the open region regionBetween with respect to the product Lebesgue measure on $\mathbf R\times\mathbf R$ ; the boundary terms are interval integrals. The hypotheses only ask for the partial derivatives $\partial_xA$ and $\partial_yB$ (as HasDerivAt along horizontal, resp. vertical, lines) and their continuity on $V$ ; no joint Fréchet differentiability is assumed.

Preamble

import Mathlib.MeasureTheory.Integral.Prod
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
set_option autoImplicit false
noncomputable section
open MeasureTheory Set

Formal statement

theorem MTT.GreenTile.green_tile_truncated_fd
    (H : ℝ) (hH : 1 < H) (A B Ax By : ℝ → ℝ → ℂ)
    (hA : ∀ x y : ℝ, |x| < 1 → 0 < y → HasDerivAt (fun s ↦ A s y) (Ax x y) x)
    (hB : ∀ x y : ℝ, |x| < 1 → 0 < y → HasDerivAt (fun t ↦ B x t) (By x y) y)
    (hAc : ContinuousOn (fun p : ℝ × ℝ ↦ A p.1 p.2) {p : ℝ × ℝ | |p.1| < 1 ∧ 0 < p.2})
    (hAxc : ContinuousOn (fun p : ℝ × ℝ ↦ Ax p.1 p.2) {p : ℝ × ℝ | |p.1| < 1 ∧ 0 < p.2})
    (hByc : ContinuousOn (fun p : ℝ × ℝ ↦ By p.1 p.2) {p : ℝ × ℝ | |p.1| < 1 ∧ 0 < p.2}) :
    (∫ p in regionBetween (fun x : ℝ ↦ Real.sqrt (1 - x ^ 2)) (fun _ ↦ H)
        (Set.Ioo (-(1 / 2)) (1 / 2)), (Ax p.1 p.2 + By p.1 p.2) ∂(volume.prod volume)) =
      (∫ x in (-(1 / 2) : ℝ)..(1 / 2), (B x H - B x (Real.sqrt (1 - x ^ 2)))) +
      (∫ x in (-(1 / 2) : ℝ)..(1 / 2),
        A x (Real.sqrt (1 - x ^ 2)) * ((-x / Real.sqrt (1 - x ^ 2) : ℝ) : ℂ)) +
      (∫ y in (Real.sqrt 3 / 2)..H, (A (1 / 2) y - A (-(1 / 2)) y)) := by sorry

Source

Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §8.2 (8.2.17)–(8.2.22); Green's theorem for a region between graphs.

View graph