Papers With

← All papers
First page of On sign patterns of Fourier coefficients of theta quotients

On sign patterns of Fourier coefficients of theta quotients

Koustav Banerjee, Kathrin Bringmann, Bernhard Heim, Ben Kane

math.NT Oct 30, 2026 · v1
formalization number-theory ai-agents
Read PDF arXiv abstract Code
TL;DR
The paper's asymptotic and sign-pattern results were formalized and verified in Lean by AxiomProver, with files in a public GitHub repository.
Abstract
Motivated by conjectures of Schlosser and Zhou on sign patterns of Fourier coefficients of infinite products, we study two families of theta quotients and their positive integral powers. We determine asymptotic formulas for their Fourier coefficients and use them to obtain explicit eventual periodic sign patterns. Our results provide new instances of the sign phenomena observed by Schlosser and Zhou and illustrate how dominant cusps determine the resulting sign patterns. These results were formalized and verified in Lean by AxiomProver.
Problem

Schlosser and Zhou conjectured eventual periodic sign patterns for the Fourier coefficients of certain infinite products. The work studies two families of theta quotients, (q,q^{m-1};q^m)^ℓ/(q^2,q^{m-2};q^m)^ℓ and their reciprocals, and the sign patterns of their coefficients.

Approach

Exact Rademacher–Zuckerman formulas for weakly holomorphic modular forms and a Tauberian-type proposition are combined with modular transformation asymptotics of theta functions near rational cusps. Dominant cusps are identified by maximizing the exponential growth term, separately for odd m, even m, and the reciprocal family with gcd(m,6)=1. AxiomProver formalized and verified the results in Lean.

Results

Asymptotic formulas for the coefficients yield explicit eventually periodic sign patterns, for example sgn(c(n)) = (-1)^n sgn(cos(π(φ_m ℓ − n/m))) for odd m and sgn = (-1)^n for even m. The Lean formalization files are publicly available.