Holomorphy of Tₚ f for holomorphic f #
Theorem statement: ModularForm.mdifferentiable_heckeT (2743fa4f-4160-5456-aeb8-0f6485a20067), by
Claude, 2026-09-05.
Proof: submission 35b46d18-227d-5c45-a94b-dc88ace693ca, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $f : \mathbb{H} \to \mathbb{C}$ be a function on the upper half-plane which is MDifferentiable
for the standard self-model-with-corners of $\mathbb{C}$ on both source and target, i.e. holomorphic
as a map between the complex manifolds $\mathbb{H}$ and $\mathbb{C}$. Let $k$ be an integer and $p$
a natural number. Then the function ModularForm.heckeT k p f, defined as the sum $\sum_{j \in \{0,\dots,p-1\}} f \mid[k] \,$heckeMatrix p j $+\; f \mid[k] \,$heckeDiagMatrix p, is again holomorphic in the same
sense, where $\mid[k]$ is the weight-$k$ slash action of $\mathrm{GL}_2(\mathbb{R})$ on functions on
$\mathbb{H}$, the matrices heckeMatrix p j are the $p$ upper-triangular representatives used in
the project's definition of heckeU, and heckeDiagMatrix p is the identity when $p = 0$ and the
element upperTriangularGL p 0 1 of $\mathrm{GL}_2(\mathbb{R})$ otherwise. No positivity, primality
or non-vanishing assumption is imposed on $p$; for $p = 0$ the first sum is empty and the statement
reduces to the holomorphy of $f \mid[k] 1$.
This is the holomorphy half of the standard statement that the Hecke operator $T_p$ preserves
holomorphic functions on $\mathbb{H}$, formulated for arbitrary functions rather than only for
modular or cusp forms. It is used when assembling $T_p$ on spaces of cusp forms, for instance in the
results producing a cusp form whose underlying function is heckeT k p f and in the computations of
$q$-expansion coefficients of $T_p$-eigenforms.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularForm_mdifferentiable_heckeT.lean
<!-- Generated by add_prove2me_provenance.py -->