The Gaussian Gabor System over the Complex Lattice Λ₃ of Gröchenig and Lyubarskii Is a Frame: A Computer-Assisted Proof

Gröchenig and Lyubarskii (Oberwolfach Report 11/2013) considered the Gabor system \(\mathcal{G}(g,\Lambda_3)\) of time-frequency shifts of the Gaussian \(g(s)\)\({}=2^{1/2}e^{-\pi|s|^2}\) on \(\mathbb{R}^2\) along the complex lattice \(\Lambda_3\)\({}=A_3(\mathbb{Z}\)\({}+i\mathbb{Z})^2\), \(A_3\)\({}=\bigl(\begin{smallmatrix}1&2/5\\0&\sqrt{21}/5\end{smallmatrix}\bigr)\). They conjectured that it is a frame for \(L^2(\mathbb{R}^2)\) and wrote that they had no reliable proof; in their paper in Complex Var. Elliptic Equ. 65 (2020), \(\Lambda_3\) is the end point \(t=\sqrt{21}/5\) of a range \(\sqrt{21}\)\(/5\)\({}\le t\)\({}<\sqrt{24}\)\(/5\) of lattices for which the answer is stated to be unknown. We prove the conjecture by a computer-assisted proof in floating point with a margin. A dilation turns \(\mathcal{G}(g,\Lambda_3)\) into a Gabor system over the rational separable lattice \(\mathbb{Z}^2\)\({}\times M\mathbb{Z}^2\), \(M\)\({}=\bigl(\begin{smallmatrix}1&2/5\\2/5&1\end{smallmatrix}\bigr)\). The fiberization of Ron and Shen and a Bloch reduction over \(5\mathbb{Z}^2\) show that the system is a frame with lower bound \((10/\sqrt{21})\,s^2\) as soon as an explicit \(25\times21\) matrix \(P(t,\theta)\) of Gaussian lattice sums satisfies \(\sigma_{\min}(P(t,\theta))\)\({}\ge s\)\({}>0\) for all \((t,\theta)\)\({}\in\mathbb{R}^4\). After a reduction by symmetries to a box in \(\mathbb{R}^4\), a branch-and-bound computation over \(65{,}597\) boxes, with a first-order bound maximised over the vertices of each box, a rigorous bound for the second-order Taylor remainder and an explicit tail bound, gives \(\sigma_{\min}(P)\)\({}\ge 0.23\) everywhere. Hence \(\mathcal{G}(g,\Lambda_3)\) is a frame with lower frame bound at least \(0.1154\) (numerically the optimal bound is \(0.12265\)). The box inequalities were evaluated in IEEE double precision with an explicit rounding budget and a margin of \(10^{-6}\), not in interval arithmetic; two independent recomputations in interval arithmetic, of the \(1950\) and of the \(2000\) boxes with the smallest margin, confirm these boxes without the margin. The same conclusion holds for the window \(e^{-\pi|s|^2/2}\), the width printed once in the report (\(\sigma_{\min}\ge0.18\)). The question and the conjecture are due to Gröchenig and Lyubarskii; no printed answer was found in the sources searched. This is an unrefereed note.