Products of convergent q-expansions on H #
Theorem statement: ModularCurve.hasSum_qParam_mul (80018164-7c58-5a39-86ee-244003282ffa), by
Claude, 2026-09-05.
Proof: submission 16c9c185-5ee9-57f9-b0aa-618fdd739fcd, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $h$ be a real number with $0 < h$, let $A, B \in \mathbb{C}[[q]]$ be formal power series over
$\mathbb{C}$, and let $F, G \colon \mathfrak{H} \to \mathbb{C}$ be arbitrary functions on the upper
half-plane. Assume that for every $\tau \in \mathfrak{H}$ the family $m \mapsto a_m\, \mathbf{q}_h(\tau)^m$, indexed by $m \in \mathbb{N}$, where $a_m$ is the $m$-th coefficient of $A$
and $\mathbf{q}_h(\tau) = \exp(2\pi i \tau / h)$ is Mathlib's Function.Periodic.qParam h (τ : ℂ),
is summable with sum $F(\tau)$; and likewise that for every $\tau \in \mathfrak{H}$ the family $m \mapsto b_m\, \mathbf{q}_h(\tau)^m$ built from the coefficients of $B$ is summable with sum
$G(\tau)$. Then for each $\tau \in \mathfrak{H}$ the family $m \mapsto c_m\, \mathbf{q}_h(\tau)^m$,
where $c_m = \sum_{i+j=m} a_i b_j$ is the $m$-th coefficient of the product power series $A \cdot B$, is summable with sum $F(\tau) G(\tau)$. Note that the hypotheses are required at every point of
$\mathfrak H$, while the conclusion is asserted at the single given point $\tau$.
This is the statement that functions realised on the upper half-plane by convergent $q$-expansions at a fixed period $h$ are closed under multiplication, with the Cauchy product of the coefficient series computing the product function. It underlies the construction of integral $q$-expansions of Siegel units and of the associated modular forms for $\Gamma_1(N)$, which invoke it when multiplying $q$-expansions and taking powers.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_hasSum_qParam_mul.lean
<!-- Generated by add_prove2me_provenance.py -->