发表机构
Center for Data Science, New York University; Department of Mathematics, MIT; Department of Mathematics, Bar-Ilan University; Mathematical Institute, University of Oxford（纽约大学数据科学中心; 麻省理工学院数学系; 巴伊兰大学数学系; 牛津大学数学研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明对形如高斯乘多项式的窗口，存在一致离散点集使短时傅里叶变换幅度唯一确定信号（至多常数相位），并给出 Lean 4 形式化证明。
AI 中文摘要
我们证明，对于形如 $w(x) = e^{-\pi|x|^2} h(x)$ 的每个窗口 $w$（其中 $h$ 为多项式），存在一个一致离散点集 $\mathcal{S} \subset \mathbb R^{2d}$，使得短时傅里叶变换 $V_w f$ 在 $\mathcal{S}$ 上的幅度决定每个 $f \in L^2(\mathbb R^d)$，且仅相差一个常数相位因子。分离距离可以选取为与 $h$ 的次数无关，并与维数的平方根成正比。证明结合了基于多维 Remez 不等式和 VC 维界的离散范数不等式，以及再生核的尾部估计。我们还提供了主要结果在 Lean 4 中的形式化。
英文摘要
We prove that for every window $w$ of the form $w(x) = e^{-π|x|^2} h(x)$, where $h$ is a polynomial, there exists a uniformly discrete set of points $\mathcal{S} \subset \mathbb R^{2d}$ such that the magnitude of the short-time Fourier transform $V_w f$ on $\mathcal{S}$ determines every $f \in L^2(\mathbb R^d)$ up to a constant phase factor. The separation distance can be chosen independent of the degree of $h$ and proportional to the square root of the dimension. The proof combines a discrete norming inequality, based on a multidimensional Remez inequality and VC-dimension bounds, with tail estimates for the reproducing kernel. A formalization of our main result in Lean 4 is also provided.
Comments14 pages, 1 figure, Lean code available at https://github.com/josefgreilhuber/DiscretePhaseRetrieval
