Wirtinger data for the two mixed-period test functions

Open

MTT.Cohomology.mixed_period_test_functions_wirtinger_data

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

complex-analysismodular-formsperiods

Let $g,v,q\in S_k(\Gamma_1(N))$ , with $k\ge2$ , and suppose that the mixed differential

g(z)(zX+Y)^{k-2}dz-\overline{v(z)}(\bar zX+Y)^{k-2}d\bar z

has a $\Gamma_1(N)$ -equivariant primitive $U$ with polynomial growth in every cusp chart. For any finite set $R\subseteq\mathrm{SL}_2(\mathbb Z)$ , there are two scalar $C^1$ test functions $A_1,A_2$ satisfying the weight-two antiholomorphic automorphy law, rapid decay at every cusp, and integrability of their Wirtinger derivatives on every tile $\sigma\mathcal D$ for $\sigma\in R$ . Their derivatives are

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

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

This packages the differential and cusp-estimate hypotheses needed to apply Stokes' theorem to both Hodge types.

Retired. The original statement could not use the correctly stated tile-integrability input because it omitted the necessary positive-level hypothesis $0<N$ . Use MTT.Cohomology.mixed_period_test_functions_wirtinger_data_of_pos_level 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.mixed_period_test_functions_wirtinger_data
    {N k : ℕ} (hk : 2 ≤ k)
    (g v q : CuspForm (MTT.GammaOne N) (k : ℤ))
    (U : ℂ → Binary ℂ) (hU : IsMixedPeriodPrimitive g v U)
    (R : Finset (Matrix.SpecialLinearGroup (Fin 2) ℤ)) :
    ∃ A₁ A₂ : ℂ → ℂ,
      ContDiffOn ℝ 1 A₁ upperHalfPlaneSet ∧
      (∀ γ ∈ CongruenceSubgroup.Gamma1 N, ∀ τ : ℍ,
        A₁ ((γ • τ : ℍ) : ℂ) =
          (starRingEnd ℂ (denom γ τ)) ^ 2 * A₁ τ) ∧
      (∀ σ : Matrix.SpecialLinearGroup (Fin 2) ℤ, IsZeroAtImInfty
        fun τ : ℍ ↦ A₁ ((σ • τ : ℍ) : ℂ) *
          ((starRingEnd ℂ (denom σ τ)) ^ 2)⁻¹) ∧
      (∀ σ ∈ R, IntegrableOn
        (fun z ↦ (1 / 2 : ℂ) *
          (fderiv ℝ A₁ z 1 - Complex.I * fderiv ℝ A₁ z Complex.I))
        ((fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟) volume) ∧
      (∀ 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 : ℂ)))) ∧
      ContDiffOn ℝ 1 A₂ upperHalfPlaneSet ∧
      (∀ γ ∈ CongruenceSubgroup.Gamma1 N, ∀ τ : ℍ,
        A₂ ((γ • τ : ℍ) : ℂ) =
          (starRingEnd ℂ (denom γ τ)) ^ 2 * A₂ τ) ∧
      (∀ σ : Matrix.SpecialLinearGroup (Fin 2) ℤ, IsZeroAtImInfty
        fun τ : ℍ ↦ A₂ ((σ • τ : ℍ) : ℂ) *
          ((starRingEnd ℂ (denom σ τ)) ^ 2)⁻¹) ∧
      (∀ σ ∈ R, IntegrableOn
        (fun z ↦ (1 / 2 : ℂ) *
          (fderiv ℝ A₂ z 1 - Complex.I * fderiv ℝ A₂ z Complex.I))
        ((fun τ : ℍ ↦ ((σ • τ : ℍ) : ℂ)) '' 𝒟) volume) ∧
      (∀ 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 : ℂ))))) := 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; the two test contractions are the standard invariant-contraction/Stokes construction.

View graph