Papers With

← All papers
First page of Derivatives of Theta Functions and a Problem of Lyubarskii and Nes

Derivatives of Theta Functions and a Problem of Lyubarskii and Nes

Lukas Liehr, Irina Shafkulovska, Mitchell A. Taylor

math.CA Aug 27, 2026 · v1 math.FA
formalization mathlib analysis
Read PDF arXiv abstract Code
TL;DR
The main frame theorem (the new direction) is formalized in Lean 4 with Mathlib, with AI assistance from Codex and Opus models.
Abstract
We characterize all lattices $Λ\subset \mathbb{R}^2$ of rational density for which the Gabor system generated by the first Hermite function along $Λ$ is a frame for $L^2(\mathbb{R})$. We prove that these are precisely the lattices whose density satisfies $D(Λ) = \frac{q}{p} $ where $p,q \in \mathbb{N}$ are coprime with $q \geq p+2$, thereby confirming a conjecture of Lyubarskii and Nes. A formalization of our main result in Lean $4$ is also included.
Problem

Lyubarskii and Nes asked which lattices of rational density give a Gabor frame for L^2(R) when generated by the first Hermite function. Their conjecture predicted the answer.

Approach

The lattice is reduced to a separable rational lattice through metaplectic covariance and the Iwasawa decomposition. The frame property is then studied through the Zak transform. The key step is a lemma on derivatives of theta functions at q equally spaced points, which rules out certain vanishing systems. The new implication is formalized in Lean 4 on top of Mathlib, using Mathlib's L^2 space and infinite sums.

Results

Such lattices give a frame exactly when D(Λ)=q/p with p and q coprime and q ≥ p+2, which confirms the conjecture. The result extends to linear combinations of h_0,…,h_n when q ≥ np+2. The sufficiency direction is machine-checked in Lean.