We prove that, after normalization, stable phase retrieval holds over the -spans of independent real-valued centered random variables if and only if all but possibly one coordinate satisfies a uniform two-sided bound. This provides a complete characterization of stable phase retrieval for such subspaces, building upon the pioneering work of Calderbank–Daubechies–Freeman–Freeman and confirming the conjectured characterization communicated to us by those authors. We provide two different proofs of this fact, both based on a decomposition of the -coefficients of each random variable. The first is a compactness proof, which makes use of the infinite divisibility of limit laws of tail sums. The second is a quantitative proof, which substitutes the compactness step with an explicit dichotomy based on anticoncentration estimates of Sperner type. This latter proof was partially LLM generated based on the ideas in the first proof and a considerable amount of guidance by the authors. An autoformalization of our main result in Lean 4 is also provided, following the ideas in the quantitative proof.

生成讲解博客的中文版本

生成AI智能校验的中文版本