Shimura's exact-form identity on the truncated tile: the Petersson-type area integral as a boundary integral

Proved

MTT.PeterssonTile.petersson_tile_stokes_fd

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

complex-analysiseichler-shimurafundamental-domainintegrationmodular-forms

Let $H>1$ , let $T_H=\{|x|<\tfrac12,\ \sqrt{1-x^2}<y<H\}$ be the truncated standard fundamental-domain tile, and let $F_p$ and $a$ be holomorphic on the upper half-plane $\mathfrak H$ . Write $\Phi(x,y)=F_p(z)\,\overline{a(z)}$ for $z=x+iy$ and $\varphi(x)=\sqrt{1-x^2}$ . Then

\iint_{T_H}F_p'(z)\,\overline{a(z)}\,dx\,dy=\frac12\left(\int_{-1/2}^{1/2}\!\big[-i\,\Phi(x,H)+i\,\Phi(x,\varphi(x))\big]dx+\int_{-1/2}^{1/2}\!\Phi(x,\varphi(x))\,\varphi'(x)\,dx+\int_{\sqrt3/2}^{H}\!\big[\Phi(\tfrac12,y)-\Phi(-\tfrac12,y)\big]dy\right).

This is Shimura's exact-form identity (8.2.17) on the tile: since $\bar a$ is antiholomorphic, $F_p'\,\bar a\,dz\wedge d\bar z=d(F_p\,\bar a\,d\bar z)$ , i.e. $2F_p'\bar a=\partial_x\Phi-i\,\partial_y\Phi$ , so the area integral of $F_p'\bar a$ is half the divergence integral of the planar field $(\Phi,-i\Phi)$ , and Green's theorem on the tile (green_tile_truncated_fd) turns it into the boundary integral $\tfrac i2\oint_{\partial T_H}\Phi\,d\bar z$ written out over the four boundary pieces (arc, right edge, top, left edge). Applied to $F_p$ a primitive of the period form $g(z)(zX+Y)^{k-2}$ (coefficientwise) and $a$ a second cusp form (so that $F_p'\bar a$ is the Petersson-type integrand), and summed over the $SL_2(\mathbf Z)$ -translates tiling a fundamental domain of $\Gamma_1(N)$ (pulled back to $T_H$ with integral_moebius_image_hyperbolic), this is the analytic core of the Eichler–Shimura pairing identity (8.2.22).

Formalization Note The area integral is over Mathlib's regionBetween with volume.prod volume; deriv Fp is the complex derivative. Holomorphy is DifferentiableOn ℂ on the open half-plane; continuity of the derivatives on the tile follows from Cauchy's theory (DifferentiableOn.deriv).

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.Complex.CauchyIntegral
set_option autoImplicit false
noncomputable section
open MeasureTheory Set

Formal statement

theorem MTT.PeterssonTile.petersson_tile_stokes_fd
    (H : ℝ) (hH : 1 < H) {Fp a : ℂ → ℂ}
    (hFp : DifferentiableOn ℂ Fp {z : ℂ | 0 < z.im})
    (ha : DifferentiableOn ℂ a {z : ℂ | 0 < z.im}) :
    (∫ p in regionBetween (fun x : ℝ ↦ Real.sqrt (1 - x ^ 2)) (fun _ ↦ H)
        (Set.Ioo (-(1 / 2)) (1 / 2)),
        deriv Fp ((p.1 : ℂ) + p.2 * Complex.I) *
          (starRingEnd ℂ) (a ((p.1 : ℂ) + p.2 * Complex.I)) ∂(volume.prod volume)) =
      (1 / 2 : ℂ) *
        ((∫ x in (-(1 / 2) : ℝ)..(1 / 2),
            (-Complex.I * (Fp ((x : ℂ) + H * Complex.I) *
                (starRingEnd ℂ) (a ((x : ℂ) + H * Complex.I))) -
              -Complex.I * (Fp ((x : ℂ) + Real.sqrt (1 - x ^ 2) * Complex.I) *
                (starRingEnd ℂ) (a ((x : ℂ) + Real.sqrt (1 - x ^ 2) * Complex.I))))) +
        (∫ x in (-(1 / 2) : ℝ)..(1 / 2),
            (Fp ((x : ℂ) + Real.sqrt (1 - x ^ 2) * Complex.I) *
              (starRingEnd ℂ) (a ((x : ℂ) + Real.sqrt (1 - x ^ 2) * Complex.I))) *
              ((-x / Real.sqrt (1 - x ^ 2) : ℝ) : ℂ)) +
        (∫ y in (Real.sqrt 3 / 2)..H,
            (Fp (((1 / 2 : ℝ) : ℂ) + y * Complex.I) *
                (starRingEnd ℂ) (a (((1 / 2 : ℝ) : ℂ) + y * Complex.I)) -
              Fp (((-(1 / 2) : ℝ) : ℂ) + y * Complex.I) *
                (starRingEnd ℂ) (a (((-(1 / 2) : ℝ) : ℂ) + y * Complex.I))))) := by sorry

Source

Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §8.2, (8.2.17)–(8.2.22).

View graph