Papers With

← All papers
First page of Phase retrieval from a uniformly discrete point set

Phase retrieval from a uniformly discrete point set

Jaume de Dios Pont, Josef Greilhuber, Lukas Liehr, Mitchell A. Taylor

math.CA Sep 23, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
The main phase retrieval uniqueness theorem is formalized in Lean 4 on top of Mathlib, with custom definitions for uniform discreteness and polyanalytic Fock spaces.
Abstract
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.
Problem

Phase retrieval asks to recover a function up to a global phase from the magnitudes of its short-time Fourier transform. The question is whether uniqueness holds when magnitudes are sampled only on a uniformly discrete point set.

Approach

For windows of the form e^{-π|x|^2}h(x) with h polynomial, the Bargmann transform identifies the STFT range with polyanalytic Fock spaces. A discrete norming inequality, built from a multidimensional Remez inequality and VC-dimension bounds, propagates smallness from a discrete set to the bulk. Tail estimates on the reproducing kernel control the truncation error. The main theorem is formalized in Lean 4 using Mathlib, with new definitions such as UniformlyDiscrete, PolyFockSpace, and PhaseRetrievalSet.

Results

There exists a uniformly discrete set S in R^{2d} such that STFT magnitudes on S determine every f in L^2(R^d) up to a constant phase. The separation distance is independent of the polynomial degree and proportional to the square root of the dimension.