The Shubin–Vakilian–Wolff Uncertainty Principle at Half Density
Ming Wang, Yunlei Wang
math.AP
Sep 12, 2026 · v1
TL;DR
Both main theorems and their extensions to all dimensions are formally verified in Lean 4 with Mathlib; the formalization was AI-generated under author guidance.
Abstract
Shubin, Vakilian, and Wolff proved a Fourier uncertainty principle for sets of sufficiently small local density at the reciprocal scale and asked whether every density below one is admissible. We answer this question negatively in dimension one by constructing sequences of pairs of $1/2$-density thin sets and unit vectors whose total position and Fourier mass outside these sets tends to zero. This obstruction persists for every scaled reciprocal profile $ρ_κ(x)=\min\{1,κ/|x|\}$, $κ>0$. On the other hand, for $0<κ\le1$, the uncertainty estimate holds whenever the density $$ \varepsilon<\frac{1}{2(1+32κ)}. $$ Thus the critical density tends to $1/2$ as $κ\downarrow 0$. The obstruction uses odd Gaussian packets to transfer norm bounds from a free-group model. The positive estimate uses a Fourier-complementary anti-Wick operator and quadratic straightening of the reciprocal geometry.
Problem
Shubin, Vakilian, and Wolff proved a Fourier uncertainty principle for sets of small local density at the reciprocal scale. They asked whether every density below one is admissible.
Approach
The negative answer in dimension one comes from a construction of 1/2-density thin sets via quadratic sets. Odd Gaussian packets transfer norm bounds from a free-group model, reduced to a half-line Jacobi operator. The positive bound uses a Fourier-complementary anti-Wick operator and a quadratic change of variables that straightens the reciprocal geometry. The results were formalized in Lean 4 with Mathlib, with the formalization generated by GPT under author guidance.
Results
The uncertainty principle fails at density 1/2 for every scaled reciprocal profile. For 0<κ≤1 it holds when ε<1/(2(1+32κ)), so the critical density tends to 1/2 as κ→0. Both main theorems and their extensions to all d≥1 are machine-checked in Lean.
