Papers With

← All papers
First page of Gabor Frames of Totally Positive Functions: A Complete Characterization

Gabor Frames of Totally Positive Functions: A Complete Characterization

Jaume de Dios Pont, Karlheinz Gröchenig, Lukas Liehr, Irina Shafkulovska, Mitchell A. Taylor

math.FA Aug 5, 2026 · v1 math.CA
formalization analysis mathlib
Read PDF arXiv abstract Code
TL;DR
Provides a Lean 4 formalization, built on Mathlib, of the sufficiency direction of the Gabor frame set theorem for totally positive functions.
Abstract
We prove that the set of time-frequency shifts $\{e^{2πi βl t} g(t-αk) : k,l \in \mathbb{Z}\}$ with a continuous, integrable totally positive function $g$ and lattice parameters $α,β>0$ generates a frame for $L^2(\mathbb{R})$ if and only if $αβ<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.
Problem

Characterizing which totally positive generators g and lattice parameters α,β yield a Gabor frame for L^2(R) is the frame set problem. Determining the exact condition had been open for this class.

Approach

The frame property is reduced via the Zak transform to invertibility of a restricted pre-Gramian matrix. Operator-theoretic tools—spectral invariance across ℓ^p spaces, Fredholm theory via band-operator approximation, and limit-operator theory—establish injectivity and hence invertibility. The nontrivial (sufficiency) direction of the main theorem is formalized in Lean 4 on top of Mathlib, using predicates IsTPIntegrableContinuous and IsGaborFrame.

Results

For a continuous, integrable totally positive g, the Gabor system is a frame if and only if αβ<1, fully settling the frame set problem for this class, plus a sharp Kadets-type theorem for the associated shift-invariant spaces. The Lean formalization verifies the sufficiency direction (αβ<1 implies frame).