On the existence problem of regular Gabor frames
Pith reviewed 2026-06-25 19:01 UTC · model grok-4.3
The pith
For d>1, explicit criteria on lattices with density >1 ensure no continuous-Zak function generates a Gabor frame.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
For every dimension d>1 there are explicit criteria on lattices Λ subset R^{2d} with D(Λ)>1 such that the Zak transforms associated to any candidate window necessarily share a common zero, so the Gabor system along Λ cannot form a frame.
What carries the argument
Characterization of common zeros for collections of quasiperiodic functions, which reduces the frame existence question to an algebraic condition on the lattice and the window.
If this is right
- No Gabor frame exists along the identified lattices for any window in the Schwartz space.
- The same lattices rule out frames generated by windows from the Feichtinger algebra and the Fourier-invariant Wiener space.
- The common-zero characterization applies directly to other questions about quasiperiodic functions.
- The negative existence result holds for every d>1 once the lattice satisfies the explicit algebraic criteria.
Where Pith is reading between the lines
- The lattice geometry alone can force unavoidable zeros in Zak transforms, independent of further regularity assumptions on the window.
- Similar algebraic obstructions might be checked computationally for concrete lattices in dimensions three and higher.
- The Lean 4 formalization shows the algebraic criterion is in principle machine-checkable.
Load-bearing premise
A collection of quasiperiodic functions admits a common zero precisely when certain explicit algebraic conditions on the lattice and the functions hold.
What would settle it
Produce a lattice meeting the stated criteria together with a continuous-Zak window whose associated quasiperiodic functions have no common zero on the fundamental domain.
Figures
read the original abstract
For every dimension $d > 1$, we establish explicit criteria on lattices $\Lambda \subset \mathbb{R}^{2d}$ with density $D(\Lambda) > 1$ such that no function with a continuous Zak transform generates a Gabor frame along $\Lambda$. In particular, this gives a negative answer to the existence problem of Gabor frames with window functions in the Schwartz space, the Feichtinger algebra, and the Fourier-invariant Wiener space. Our result is based on a characterization of when a collection of quasiperiodic functions admits a common zero, which may be of independent interest. We also include a formalization of our main result in Lean 4.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper establishes explicit criteria on lattices Λ ⊂ ℝ^{2d} (d > 1) with density D(Λ) > 1 such that no function possessing a continuous Zak transform generates a Gabor frame along Λ. This yields negative answers to the existence of regular Gabor frames with windows in the Schwartz space, Feichtinger algebra, and Fourier-invariant Wiener space. The argument rests on a new algebraic characterization of when collections of quasiperiodic functions admit a common zero; the main result is formalized in Lean 4.
Significance. If the result holds, it supplies concrete obstructions that resolve an open existence question in time-frequency analysis for highly regular windows on overcomplete lattices. The characterization of common zeros for quasiperiodic functions is of independent interest, and the Lean 4 formalization provides machine-checked verification of the central derivation, strengthening the reliability of the algebraic reduction from the frame condition to the zero-set condition.
minor comments (2)
- The abstract and introduction would benefit from a brief statement of the precise form of the explicit criteria on the lattice (e.g., the algebraic conditions on the generators of Λ) to allow readers to assess applicability without reading the full characterization section.
- Notation for the Zak transform and the quasiperiodic functions could be introduced with a short reminder of their periodicity properties in §2 to improve readability for readers outside the immediate subfield.
Simulated Author's Rebuttal
We thank the referee for the positive report, the recognition of the significance of our results, and the recommendation to accept the manuscript. We appreciate the comments on the independent interest of the algebraic characterization and the Lean 4 formalization.
Circularity Check
No significant circularity; derivation self-contained via machine-checked characterization
full rationale
The paper's central step converts the Gabor frame question into a common-zero question for quasiperiodic functions via an explicit algebraic characterization on the lattice. This characterization is formalized and verified in Lean 4, supplying direct machine-checked support independent of the present paper's fitted values or self-referential definitions. No load-bearing self-citation chains, ansatzes smuggled via prior work, or predictions that reduce to inputs by construction are present. The result is externally falsifiable via the formalization and applies to standard function spaces without redefining its own premises.
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Standard properties of the Zak transform and Gabor systems in L2(R^d) as developed in prior literature.
Reference graph
Works this paper leans on
-
[1]
Formalization of De Giorgi–Nash–Moser Theory in Lean
Scott Armstrong and Julia Kempe. Formalization of De Giorgi–Nash–Moser Theory in Lean. arXiv preprint arXiv:2604.05984 , 2026
Pith/arXiv arXiv 2026
-
[2]
Abelian Harmonic Analysis, Theta Functions and Functional Algebras on a Nilmanifold
Louis Auslander and Richard Tolimieri. Abelian Harmonic Analysis, Theta Functions and Functional Algebras on a Nilmanifold . Springer, 2006
2006
-
[3]
Smooth lattice orbits of nilpotent groups and strict comparison of projections
Erik Bédos, Ulrik Enstad, and Jordy Timo van Velthoven. Smooth lattice orbits of nilpotent groups and strict comparison of projections. J. Funct. Anal. , 283(6):109572, 2022
2022
-
[4]
Square integrable representations, von Neumann algebras and an application to Gabor analysis
Bachir Bekka. Square integrable representations, von Neumann algebras and an application to Gabor analysis. J. Fourier Anal. Appl. , 10(4):325–349, 2004
2004
-
[5]
Gabor frames for rational functions
Yurii Belov, Aleksei Kulikov, and Yurii Lyubarskii. Gabor frames for rational functions. Invent. Math. , 231(2):431–466, 2023
2023
-
[6]
Susanna Bertolini, Jaume de Dios Pont, Ben Pineau, Mitchell A. Taylor, and João P. G. Ramos. L2-Stability for STFT phase retrieval. arXiv preprint arXiv:2605.20527 , 2026
Pith/arXiv arXiv 2026
-
[7]
Boon and J
M. Boon and J. Zak. Amplitudes on von Neumann lattices. J. Math. Phys. , 22(5):1090–1099, 1981
1981
-
[8]
T. W. Chaundy and A. E. Jolliffe. The uniform convergence of a certain class of trigono- metrical series. Proc. Lond. Math. Soc. , 2(1):214–216, 1917. ON THE EXISTENCE PROBLEM OF REGULAR GABOR FRAMES 25
1917
-
[9]
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28: 28th International Conference on Au- tomated Deduction, Virtual Event, July 12–15, 2021, Proceedings , page 625–635, Berlin, Heidelberg, 2021. Springer-Verlag
2021
-
[10]
Lean Theorem Prover MCP
Oliver Dressler. Lean Theorem Prover MCP. https://github.com/oOo0oOo/lean-lsp-mcp , 2026
2026
-
[11]
The Balian–Low theorem for locally compact abelian groups and vector bun- dles
Ulrik Enstad. The Balian–Low theorem for locally compact abelian groups and vector bun- dles. J. Math. Pures Appl , 139:143–176, 2020
2020
-
[12]
Jakobsen, Franz Luef, and Tron Omland
Ulrik Enstad, Mads S. Jakobsen, Franz Luef, and Tron Omland. Deformations and Balian- Low theorems for Gabor frames on the adeles. Adv. Math. , 410:108771, 2022
2022
-
[13]
Criteria for the existence of Schwartz Gabor frames over rational lattices
Ulrik Enstad, Hannes Thiel, and Eduard Vilalta. Criteria for the existence of Schwartz Gabor frames over rational lattices. Int. Math. Res. Not. IMRN , 2025(5), 2025
2025
-
[14]
Z-stability of twisted group C ∗-algebras of nilpotent groups
Ulrik Enstad and Eduard Vilalta. Z-stability of twisted group C ∗-algebras of nilpotent groups. arXiv:2503.18088, 2026
Pith/arXiv arXiv 2026
-
[15]
Feichtinger
Hans G. Feichtinger. On a new Segal algebra. Monatsh. Math. , 92(4):269–289, 1981
1981
-
[16]
Grepstad and M
S. Grepstad and M. N. Kolountzakis. Bounded common fundamental domains for two lat- tices. Adv. Math. , 487:110776, 2026
2026
-
[17]
Multivariate Gabor frames and sampling of entire functions of several variables
Karlheinz Gröchenig. Multivariate Gabor frames and sampling of entire functions of several variables. Appl. Comput. Harmon. Anal. , 31(2):218–227, 2011
2011
-
[18]
Totally positive functions and Gabor frames over rational lattices
Karlheinz Gröchenig. Totally positive functions and Gabor frames over rational lattices. Adv. Math. , 427:109113, 2023
2023
-
[19]
Sampling of entire functions of several com- plex variables on a lattice and multivariate Gabor frames
Karlheinz Gröchenig and Yurii Lyubarskii. Sampling of entire functions of several com- plex variables on a lattice and multivariate Gabor frames. Complex Var. Elliptic Equ. , 65(10):1717–1735, 2020
2020
-
[20]
Balian–Low type theorems on homogeneous groups
Karlheinz Gröchenig, José Luis Romero, David Rottensteiner, and Jordy Timo Van Velthoven. Balian–Low type theorems on homogeneous groups. Analysis Mathemat- ica, 46(3):483–515, 2020
2020
-
[21]
Gabor frames and totally positive functions
Karlheinz Gröchenig and Joachim Stöckler. Gabor frames and totally positive functions. Duke Math. J. , 162(6):1003–1031, 2013
2013
-
[22]
Foundations of Time-Frequency Analysis
Karlheinz Gröchenig. Foundations of Time-Frequency Analysis . Birkhäuser Basel, 2001
2001
-
[23]
Sampling theorems for shift- invariant spaces, Gabor frames, and totally positive functions
Karlheinz Gröchenig, José Luis Romero, and Joachim Stöckler. Sampling theorems for shift- invariant spaces, Gabor frames, and totally positive functions. Invent. Math. , 211:1119– 1148, 2018
2018
-
[24]
Differential topology, volume 370
Victor Guillemin and Alan Pollack. Differential topology, volume 370. American Mathemat- ical Society, 2025
2025
-
[25]
Lattice tiling and the Weyl-Heisenberg frames
Deguang Han and Yang Wang. Lattice tiling and the Weyl-Heisenberg frames. Geom. Funct. Anal., 11(4):742–758, 2001
2001
-
[26]
A Milestone in Formalization: The Sphere Pack- ing Problem in Dimension 8
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska. A Milestone in Formalization: The Sphere Pack- ing Problem in Dimension 8. arXiv preprint arXiv:2604.23468 , 2026
Pith/arXiv arXiv 2026
-
[27]
History and evolution of the density theorem for Gabor frames
Christopher Heil. History and evolution of the density theorem for Gabor frames. J. Fourier Anal. Appl., 13(2):113–166, 2007
2007
-
[28]
Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium
Vasily Ilin. Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. arXiv preprint arXiv:2603.15929 , 2026
arXiv 2026
-
[29]
Jakobsen and Franz Luef
Mads S. Jakobsen and Franz Luef. Duality of Gabor frames and Heisenberg modules. J. Noncommut. Geom., 14(4):1445–1500, 2020
2020
-
[30]
A. J. E. M. Janssen. Bargmann transform, Zak transform, and coherent states. J. Math. Phys., 23(5):720–731, 1982
1982
-
[31]
Zeros of the Zak transform on locally compact Abelian groups
Eberhard Kaniuth and Gitta Kutyniok. Zeros of the Zak transform on locally compact Abelian groups. Proc. Amer. Math. Soc. , 126(12):3561–3569, 1998
1998
-
[32]
The structure of some induced representations
Adam Kleppner. The structure of some induced representations. Duke Math. J. , 29:555–572, 1962
1962
-
[33]
John M. Lee. Introduction to Smooth Manifolds . Springer New York, 2012. 26 JAUME DE DIOS PONT, LUKAS LIEHR, AND MITCHELL A. TAYLOR
2012
-
[34]
Full Gabor frames, its existence problem, and a non-uniform Balian-low type theorem
Rui Liu, Xin Ma, and Yuxuan Zheng. Full Gabor frames, its existence problem, and a non-uniform Balian-low type theorem. arXiv preprint arXiv:2606.19800 , 2026
Pith/arXiv arXiv 2026
-
[35]
A characterization of the minimal strongly character invariant Segal algebra
Viktor Losert. A characterization of the minimal strongly character invariant Segal algebra. Ann. Inst. Fourier (Grenoble) , 30(3):129–139, 1980
1980
-
[36]
Gaussian Gabor frames, Seshadri constants and generalized Buser–Sarnak invariants
Franz Luef and Xu Wang. Gaussian Gabor frames, Seshadri constants and generalized Buser–Sarnak invariants. Geom. Funct. Anal. , 33(3):778–823, 2023
2023
-
[37]
Frames in the Bargmann space of entire functions
Yurii Lyubarskii. Frames in the Bargmann space of entire functions. In Entire and sub- harmonic functions , volume 11 of Adv. Soviet Math. , pages 167–180. Amer. Math. Soc., Providence, RI, 1992
1992
-
[38]
Topology from the differentiable viewpoint, Univ
John Milnor. Topology from the differentiable viewpoint, Univ . Press of Virginia, Char- lottesville, 1965
1965
-
[39]
Stasheff
John Willard Milnor and James D. Stasheff. Characteristic classes . Number 76 in Annals of Mathematics Studies. Princeton University Press, 1974
1974
-
[40]
Pfander, Peter Rashkov, and Yang Wang
Götz E. Pfander, Peter Rashkov, and Yang Wang. A geometric construction of tight mul- tivariate Gabor frames with compactly supported smooth windows. J. Fourier Anal. Appl. , 18(2):223–239, 2012
2012
-
[41]
Sampling in the shift-invariant space generated by the bivariate Gaussian function
José Luis Romero, Alexander Ulanovskii, and Ilya Zlotnikov. Sampling in the shift-invariant space generated by the bivariate Gaussian function. J. Funct. Anal. , 287(9):110600, 2024
2024
-
[42]
Density theorems for sampling and interpolation in the Bargmann-Fock space I
Kristian Seip. Density theorems for sampling and interpolation in the Bargmann-Fock space I. J. Reine Angew. Math. , 1992(429):91–106, 1992
1992
-
[43]
Density theorems for sampling and interpolation in the Bargmann-Fock space II
Kristian Seip and Robert Wallstén. Density theorems for sampling and interpolation in the Bargmann-Fock space II. J. Reine Angew. Math. , 429:107–114, 1992
1992
-
[44]
The Lean Mathematical Library
The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2020, New Orleans, LA, USA, January 2020. ACM
2020
-
[45]
O. L. Vinogradov and A. Y. Ulitskaya. Zeros of the Zak Transform of averaged totally positive functions. J. Approx. Theory , 222:55–63, 2017
2017
-
[46]
Tauberian theorems
Norbert Wiener. Tauberian theorems. Ann. of Math. , 33(1):1–100, 1932. Center for Data Science, New York University, New York, New York 10011, USA Email address : jdedios@nyu.edu Department of Mathematics, Bar-Ilan University, Ramat-Gan 5290002, Israel Email address : lukas.liehr@biu.ac.il Department of Mathematics, ETH Zürich, Ramistrasse 101, 8092 Züric...
1932
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.