q-expansion of f(dτ): coefficients shifted by d #
Theorem statement: UpperHalfPlane.qCoeff_comp_heckeDiagMatrix_smul
(9cbe736c-cda2-5e3a-b708-dbc4e42582e4), by Claude, 2026-09-05.
Proof: submission 276b173c-b4da-596b-b834-943f491bcf70, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $f : \mathbb{H} \to \mathbb{C}$ be a function on the upper half-plane subject to three
hypotheses: the composite of UpperHalfPlane.ofComplex with $f$ is periodic with period $1$ as a
function on $\mathbb{C}$; $f$ is holomorphic, in the sense of being MDifferentiable for the
standard model with corners of $\mathbb{C}$ over itself on both source and target; and $f$ is
bounded at $i\infty$ (UpperHalfPlane.IsBoundedAtImInfty). Let $d$ be a natural number with $d \neq 0$ and let $n$ be a natural number. Here ModularForm.heckeDiagMatrix d is, for $d \neq 0$, the element of
$\mathrm{GL}_2(\mathbb{R})$ given by the upper triangular matrix $\begin{pmatrix} d & 0 \\ 0 & 1\end{pmatrix}$ (and $1$ when $d = 0$), so that its action on $\mathbb{H}$ sends $\tau$ to $d\tau$;
and ModularFormClass.qCoeff g n denotes the $n$-th
coefficient of the $q$-expansion of $g$ taken with respect to the period $1$. The assertion is that
the $n$-th such coefficient of $\tau \mapsto f(\mathrm{heckeDiagMatrix}\, d \cdot \tau)$ equals the
$(n/d)$-th coefficient of $f$ when $d \mid n$, and $0$ otherwise.
This is the coefficient formula for the degeneracy (oldform) operator $V_d : \sum_n a_n q^n \mapsto \sum_n a_n q^{dn}$, stated for bare functions on $\mathbb{H}$ rather than for elements of a space of modular forms, so that it applies before any slash-invariance is recorded. It is used throughout the level-lowering and oldform bookkeeping, for instance in the analysis of eigenforms under the operators $U_\ell$ and the degeneracy maps between levels.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_UpperHalfPlane_qCoeff_comp_heckeDiagMatrix_smul.lean
<!-- Generated by add_prove2me_provenance.py -->