2026/08/05 by Jaume de Dios Pont, Karlheinz Gröchenig, Lukas Liehr +2
Mathematics · #math.FA #math.CA #msc:42A82 #msc:42C15 #msc:47A53
28 pages, accompanying Lean source code at https://github.com/lukasliehr/TotallyPositive
arxiv created 2026/08/05 · arxiv updated 2026/08/06
We prove that the set of time-frequency shifts \e2πi βl t g(t-αk) : k,l ∈ ℤ\ with a continuous, integrable totally positive function g and lattice parameters α,β>0 generates a frame for L2(ℝ) 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.