Uₚ f is bounded at every cusp #
Theorem statement: ModularFormClass.isBoundedAt_heckeU (9e99632d-bbbf-5a55-9d7e-eb14a1471767),
by Claude, 2026-09-05.
Proof: submission 1be9a414-4aa1-56c6-aa58-e07600186dd3, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ be a type whose elements act as functions from the upper half-plane $\mathbb{H}$ to
$\mathbb{C}$, let $\Gamma$ be a subgroup of $\mathrm{GL}_2(\mathbb{R})$ satisfying
Subgroup.IsArithmetic, let $k$ be an integer, and assume ModularFormClass F \Gamma k, so that
each element of $F$ is a weight-$k$ modular form for $\Gamma$ (in particular holomorphic,
slash-invariant and bounded at the cusps of $\Gamma$). Let $f : F$, let $p$ be a natural number, and
let $c \in \mathbb{P}^1(\mathbb{R}) =$ OnePoint ℝ be a cusp of $\Gamma$, i.e. IsCusp c Γ holds.
The conclusion is that the function $$\mathrm{heckeU}\,k\,p\,f \;=\; \sum_{j \in \{0,\dots,p-1\}} f \mid_k \mathrm{heckeMatrix}\,p\,j,$$ where $\mathrm{heckeMatrix}\,p\,j$ is the identity when $p = 0$
and otherwise the upper triangular matrix $\begin{pmatrix} 1 & j \\ 0 & p\end{pmatrix} \in \mathrm{GL}_2(\mathbb{R})$, is bounded at $c$ in weight $k$ in the sense of OnePoint.IsBoundedAt.
No condition relating $p$ to the level of $\Gamma$ is imposed, and for $p = 0$ the sum is empty, so
the assertion is then boundedness of the zero function.
This is the cusp-boundedness half of the statement that the Hecke operator $U_p$ preserves
weight-$k$ modular forms; together with holomorphy and slash-invariance it supplies the
bdd_at_cusps condition needed to view $U_p f$ as a modular form on a congruence subgroup. It is
used in the study of $q$-expansions and function fields of modular curves, for instance in the
comparison of $q$-expansion function fields for $\Gamma_0$-level structures and in the
identification of the function field at full level for level two.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularFormClass_isBoundedAt_heckeU.lean
<!-- Generated by add_prove2me_provenance.py -->