AI 中文总结
该研究刻画了连续可积完全正函数的Gabor框架生成条件，解决了其框架集问题，证明了相关Kadets型定理，基于Fredholm等理论完成证明并给出Lean 4形式化。
AI 中文摘要
我们证明，对于连续可积的完全正函数g，以及格参数α,β>0，时频平移集{e^{2πiβlt}g(t−αk):k,l∈ℤ}生成L²(ℝ)的框架当且仅当αβ<1。这完全解决了完全正函数类的所谓框架集问题。作为紧密相关的结果，我们为每个由连续完全正函数生成的平移不变空间证明了一个尖锐的Kadets型定理。证明基于Fredholm理论和极限算子理论。我们还提供了主要结果在Lean 4中的形式化。
英文摘要
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.
Comments28 pages, accompanying Lean source code at https://github.com/lukasliehr/TotallyPositive
