Papers With

← All papers
First page of Universal completeness of exponentials

Universal completeness of exponentials

Susanna Bertolini, Enric Florit-Simon, Lukas Liehr, Mitchell A. Taylor

math.CA Sep 17, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Main Fourier uniqueness and completeness theorems for exponential systems are formalized and verified in Lean using Mathlib.
Abstract
We consider generalizations of the classical Fourier uniqueness theorem. First, we construct a family of uniformly discrete sets $Λ\subset \mathbb{R}$, of uniform density one, such that the exponential system $\{e^{2πiλx} : λ\in Λ\}$ is complete in $L^p(S)$ for every $1 \leq p < \infty$ and every measurable set $S \subset \mathbb{R}$ with $|S| < 1$. We also show that no set that is asymptotically integer can have this universality property. Additionally, for every $v \in (0,1)$, we construct a set of integer frequencies and uniform density $v$ whose exponential system is complete in $L^p(S)$ for every $1 \leq p < \infty$ and every measurable set $S \subset [0,1]$ with $|S| < v$. Finally, we prove that the Sobolev regularity condition $α> \frac12$ for the existence of uniformly discrete uniqueness sets for spectra with periodic weak gaps, considered by Olevskii and Ulanovskii, is sharp. Our findings admit extensions to higher dimensions and are verified in Lean.
Problem

Classical Fourier uniqueness concerns which exponential systems E(Λ) are complete in L^p spaces. The authors study universal completeness: fixing frequency sets Λ complete on all measurable sets of measure below a threshold, and sharpness of Sobolev regularity conditions for uniqueness sets with periodic weak gaps.

Approach

They construct uniformly discrete sets of uniform density one whose exponential systems are complete in L^p(S) for every measurable S with |S|<1, using perturbations of integers driven by irrational rotations and ergodic-theoretic and complex-analytic tools. They also build integer-frequency sets of arbitrary density v with completeness on subsets of [0,1], and prove sharpness of the Sobolev exponent α>1/2 via iterative interpolation constructions. Results extend to higher dimensions. The main statements are formalized in Lean relying on Mathlib, with Showcase.lean files presenting checked statements accessible to non-Lean users.

Results

They obtain universal completeness sets of density one, show asymptotically integer frequencies cannot have this property, construct density-v universal integer frequency sets, and prove the Sobolev threshold α>1/2 is sharp. The corresponding uniqueness and nonuniqueness statements are machine-verified in Lean.