Gabor Frames of Totally Positive Functions: A Complete Characterization

Abstract

We prove that the set of time-frequency shifts $\{e^{2\pi i\beta lt}g(t-\alpha k):k,l\in \mathbb{Z}\}$ with a continuous, integrable totally positive function $g$ and lattice parameters $\alpha ,\beta >0$ generates a frame for $L^2(\mathbb{R})$ if and only if $\alpha \beta <1$. This fully settles the so-called frame set problem for the class of totally positive functions. As a closely related result we prove a sharp Kadets-type theorem for every shift-invariant space generated by a continuous totally positive function. The proofs are based on Fredholm theory and limit-operator theory. A formalization of our main result in Lean 4 is also provided.

28 pages, accompanying Lean source code at https://github.com/lukasliehr/TotallyPositive