Random Matrix Theory

Motivation

Many data sets are large matrices of which only a small fraction of the entries is observed, and of which the underlying object is believed to have low rank: user–item rating tables in collaborative filtering, distance matrices in sensor-network localization, and measurement matrices in structure-from-motion. Matrix completion asks when the missing entries can be recovered exactly. Rank minimization subject to the observed entries is intractable in general. Its convex relaxation, nuclear-norm minimization, is a semidefinite program, and the question is how many randomly placed entries it needs.

Timeline:

• 2008–2009. Candès and Recht (arXiv:0805.4471) proved that nuclear-norm minimization recovers an incoherent $n\times n$ matrix of rank $r$ from about $\mu_0 n^{6/5} r\log n$ uniformly sampled entries, and from $n^{5/4}$ in the low-rank regime. They also showed that about $\mu_0 nr\log n$ entries are necessary for any method.
• 2010. Candès and Tao (doi:10.1109/TIT.2010.2044061), the source of this mission, closed most of the gap. Under a strong incoherence assumption, $C\mu^2 nr\log^6 n$ entries suffice (Theorem 1.2), within a polylogarithmic factor of the information-theoretic limit, which the same paper sharpens (Theorem 1.7).
• 2009–2011. Keshavan, Montanari and Oh (arXiv:0901.3150) obtained comparable bounds for a non-convex method. Gross (arXiv:0910.1879) and Recht (arXiv:0910.0651) later gave much shorter proofs of an $O(\mu_0 nr\log^2 n)$ bound under a different incoherence condition, using matrix Bernstein inequalities and a "golfing" construction of the dual certificate.

Setting

Fix $M \in \mathbb{R}^{n\times n}$ of rank $r$ with singular value decomposition $M = \sum_{k=1}^r\sigma_k u_kv_k^*$, where $\sigma_k>0$ and $\{u_k\}$, $\{v_k\}$ are orthonormal. Let $P_U = \sum_k u_ku_k^*$, $P_V = \sum_k v_kv_k^*$, and let $E = \sum_k u_kv_k^*$ be the sign matrix. The tangent space $T$ at $M$ is the image of the projection

$$\mathcal{P}_T(X) = P_UX + XP_V - P_UXP_V,$$

and $\mathcal{P}_{T^\perp} = \mathcal{I} - \mathcal{P}_T$.

$M$ obeys the strong incoherence property with parameter $\mu$ if every entry of $P_U$ and $P_V$ is within $\mu\sqrt r/n$ of the corresponding entry of $(r/n)I$, and every entry of $E$ is at most $\mu\sqrt r/n$ in absolute value.

An observation set $\Omega \subseteq [n]\times[n]$ is either a uniformly random $m$-subset (the uniform model) or contains each entry independently with probability $p = m/n^2$ (the Bernoulli model). $\mathcal{P}_\Omega$ keeps the entries in $\Omega$ and zeroes the rest. The program is

$$\text{minimize } \|X\|_* \text{ subject to } \mathcal{P}_\Omega(X) = \mathcal{P}_\Omega(M), \qquad \text{(I.3)}$$

where $\|X\|_*$ is the sum of the singular values.

The analysis uses the centered operators $\mathcal{Q}_\Omega = p^{-1}\mathcal{P}_\Omega - \mathcal{I}$ and $\mathcal{Q}_T = \mathcal{P}_T - \rho'\mathcal{I}$, where $\rho = r/n$ and $\rho' = 2\rho-\rho^2$. It also uses the random matrices $(\mathcal{Q}_\Omega\mathcal{Q}_T)^k\mathcal{Q}_\Omega(E)$, where the operator is applied to $E$ from the right. $\|\cdot\|$ denotes the spectral norm.

Formalization targets

Goal: Theorem 1.2 (Matrix Completion II)

There is an absolute constant $C>0$ such that, for every fixed $M$ as above and $m \le n^2$ uniformly sampled entries,

$$m \ge C\mu^2 nr\log^6 n \implies \Pr\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.$$

The constant $C$ is not fixed; the goal asserts only its existence.

Milestones (in attack order)

1. Lemma 3.1. A dual certificate $Y$ with $\mathcal{P}_\Omega(Y)=Y$, $\mathcal{P}_T(Y)=E$, $\|\mathcal{P}_{T^\perp}(Y)\|<1$, together with injectivity of $\mathcal{P}_\Omega$ on $T$, implies unique recovery. This is already proved on the platform.
2. Theorem 3.2 (Rudelson selection estimate). With probability at least $1-3n^{-\beta}$,

$$p^{-1}\|\mathcal{P}_T\mathcal{P}_\Omega\mathcal{P}_T - p\mathcal{P}_T\| \le C_R\sqrt{\mu_0nr\beta\log n/m},$$

provided the right-hand side is below $1$. 3. Lemma 8.1. An exact expansion of $(\mathcal{Q}_\Omega\mathcal{P}_T)^k\mathcal{Q}_\Omega$ in powers of $\mathcal{Q}_\Omega\mathcal{Q}_T$ with explicit recursive coefficients. 4. Lemma 8.2. The coefficients are at most $\lambda^{\lceil (k-j)/2\rceil}4^k$, with $\lambda = \rho'/p$. 5. Lemma 3.3. On the event $\|(\mathcal{Q}_\Omega\mathcal{Q}_T)^k\mathcal{Q}_\Omega(E)\| \le \sigma^{(k+1)/2}$, the same terms with $\mathcal{P}_T$ obey the bound with an extra factor $1+4^{k+1}$. 6. Theorem 3.6 (Moment bound II). Let $A = (\mathcal{Q}_\Omega\mathcal{Q}_T)^k\mathcal{Q}_\Omega(E)$ and $r_\mu = \mu^2 r$. Then

$$\mathbb{E}\operatorname{trace}\bigl((A^*A)^j\bigr) \le n\bigl(C(j(k+1))^6nr_\mu/m\bigr)^{j(k+1)}.$$

7. Corollary 3.7. Under (I.12), with probability at least $1-n^{-3}$ the certificate (III.10) exists and has $\|\mathcal{P}_{T^\perp}(Y)\|\le 1/2$.

Significance

Theorem 1.2 shows that a polynomial-time convex program recovers an incoherent low-rank matrix from a number of entries that is linear in $nr$ and within a polylogarithmic factor of what any method requires. It turned nuclear-norm minimization from a heuristic into a method with near-optimal guarantees, and much of the later work on low-rank recovery, robust PCA and phase retrieval uses its framework of dual certificates, tangent spaces and incoherence.

The theorem is proved; formalizing it is the remaining work here. None of these results has a machine-checked proof. The platform already has the Candès–Recht definitions (nuclear norm, SVD data, Bernoulli model, tangent projection), the deterministic Lemma 3.1, and the Bernoulli-to-uniform transfer. This mission adds:

• the trace-moment bound, which is the combinatorial core of the paper;
• the deterministic operator algebra of Appendix A;
• the assembly into the main theorem.

Shorter later proofs (Gross, Recht) use a different incoherence condition. A formal proof of the goal along either route is welcome, provided it proves the statement as given.

Difficulty

The obvious approach bounds each term $\|(\mathcal{Q}_\Omega\mathcal{P}_T)^k\mathcal{Q}_\Omega(E)\|$ of the Neumann series for the certificate separately, using noncommutative Khintchine inequalities and decoupling. This is what Candès and Recht did, and it fails beyond small $k$: the entries of these matrices are coupled through the same random indicators, and the bounds degrade with $k$. That is where their $n^{6/5}$ comes from.

The moment method avoids this but has its own obstruction. Taking absolute values inside the expansion of $\mathbb{E}\operatorname{trace}(A^*A)^j$ loses a factor of $r$, which gives the quadratic dependence of Theorem 1.1. The linear bound needs sign cancellations among the coefficients of $\mathcal{Q}_T$ to be tracked through a nested induction over "generalized spider" configurations (Section VI). Replacing $\mathcal{P}_T$ by $\mathcal{Q}_T$ (Lemma 3.3) is necessary for those cancellations. Without it the diagonal coefficients are of size $r/n$ instead of $\sqrt r/n$.

Formalization scope

• Objects. Matrices are Matrix (Fin n) (Fin n) ℝ (MatrixCompletion.RealMatrix). The SVD is the platform structure SVD M r. Logarithms are natural. Probabilities are the platform's finite sums: successProb (uniform $m$-subsets), bernoulliEventProb and bernoulliExpectation. The spectral norm is spectralNorm. The definitions of matrix_completion_{basic,svd,bernoulli,tangent} are reused, not restated.
• Square case. Theorem 1.2 is printed "under the same hypotheses as in Theorem 1.1", for $n_1\times n_2$ matrices. The paper proves only $n_1=n_2=n$ (Section I-H), and the goal and milestones 3–7 are square. Theorem 3.2 is quoted from Candès–Recht and is stated rectangular, as printed.
• Rank. "The same hypotheses" is read as the matrix hypotheses (fixed $M$, strong incoherence, uniform sampling), not as $r = O(1)$: (I.12) carries $r$, the paper calls the result general and nonasymptotic, and Section VI never uses bounded rank. The goal holds for every $r$.
• Constants. Every "numerical constant" ($C$, $C_R$, $c_0$) and every $O(\cdot)$ is an existential absolute constant quantified before all other variables. The goal's $C$ absorbs the standing assumptions $n \ge C'$ and $m\ge 2nr$. Where a milestone needs (I.22), $2nr\le m$ is an explicit hypothesis, and $m\le n^2$ is explicit wherever a probability or $p\le 1$ appears.
• Correction of Theorem 3.6. The printed bound (III.27) omits the factor $n$ and the $O(1)^{j(k+1)}$ constant of the paper's own final display (p. 2070), and as printed it is false: for $k=0$, $j=1$ and a flat rank-one matrix, the left side exceeds the right by the factor $n(1-p)$. The formal statement is the bound the paper derives, $n\,(C(j(k+1))^6nr_\mu/m)^{j(k+1)}$, under $nr_\mu\le m$, which that derivation uses and which (I.12) implies. The milestone text is kept verbatim.
• Deterministic lemmas. Lemmas 3.3, 8.1 and 8.2 hold for every fixed $\Omega$. The event (III.18) is a hypothesis, not a probability.
• Certificate. $Y$ of (III.10) exists only when $\mathcal{P}_\Omega$ is injective on $T$, so Corollary 3.7's event includes injectivity. $Y$ is characterized as the minimum-Frobenius-norm solution of $\mathcal{P}_\Omega(Y)=Y$, $\mathcal{P}_T(Y)=E$ (p. 2061).
• Ruling out trivialization. The hypothesis $m\le n^2$ is there only because successProb is $0$ for $m>n^2$; it does not exclude any case the paper covers. The failure probability stays $n^{-3}$ and is not traded for a constant. The constant $C$ may not depend on $n$, $r$, $\mu$ or $M$, so it cannot be chosen to make (I.12) unsatisfiable. For fixed $C$, (I.12) is satisfiable with $m \le n^2$ for every large $n$ and every $r \le n/(C\mu^2\log^6 n)$.
• Not covered. Proposition 6.1 (the summand bound on generalized spiders) is the heart of Theorem 3.6. It needs the admissible-quadruplet combinatorics of Sections IV–VI as definitions, and is left to solvers as a lemma of their own. Contributions formalizing Sections IV–VI (the moment expansion (IV.10), admissible pairs, the cancellation identities (VI.1)–(VI.4)) are welcome and reusable for mission I of this series.

Selected references

• E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
• E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://arxiv.org/abs/0805.4471
• R. H. Keshavan, A. Montanari and S. Oh, Matrix Completion from a Few Entries, IEEE Trans. Inf. Theory 56(6):2980–2998, 2010. https://arxiv.org/abs/0901.3150
• D. Gross, Recovering Low-Rank Matrices from Few Coefficients in Any Basis, IEEE Trans. Inf. Theory 57(3):1548–1566, 2011. https://arxiv.org/abs/0910.1879
• B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://arxiv.org/abs/0910.0651

Motivation

Matrix completion asks to recover a low-rank matrix from a small random subset of its entries. It models collaborative filtering (a ratings matrix with most entries missing), sensor-network localization from partial distance matrices, and system identification. The natural estimator, the matrix of least rank that agrees with the observations, is NP-hard to compute in general. Candès and Recht (Found. Comput. Math. 2009) proposed to replace the rank by the nuclear norm (the sum of the singular values), its convex envelope, and proved that this convex program recovers the matrix exactly from $O(n^{6/5} r \log n)$ random entries under incoherence assumptions.

Candès and Tao (IEEE Trans. Inf. Theory 2010) sharpened the sample size to within logarithmic factors of the information-theoretic minimum $n r\log n$. This mission formalizes their first result, Theorem 1.1, whose proof is a direct moment computation, together with the lemmas on which that proof rests.

Timeline:

• 2009, Candès–Recht: exact recovery from $m \gtrsim \mu_0 n^{6/5} r \log n$ entries.
• 2010, Candès–Tao (this paper): $m \gtrsim \mu^4 n r^2 (\log n)^2$ (Theorem 1.1, general-rank form) and $m \gtrsim \mu^2 n r \log^6 n$ (Theorem 1.2), plus a lower bound of order $n r \log n$ for every method (Theorem 1.7).
• 2011, Gross (IEEE Trans. Inf. Theory) and Recht (JMLR): $m \gtrsim \mu_0 n r \log^2 n$ by the "golfing scheme", with a different proof.

Setting

Let $M \in \mathbb R^{n\times n}$ have rank $r$ and singular value decomposition $M = \sum_{k=1}^r \sigma_k u_k v_k^*$ with $\sigma_k > 0$ and orthonormal $u_k$, $v_k$. Write $P_U = \sum_k u_k u_k^*$, $P_V = \sum_k v_k v_k^*$ and $E = \sum_k u_k v_k^*$. The matrix obeys the strong incoherence property with parameter $\mu > 0$ if, for all indices $a, a', b, b'$,

$$\Bigl|\langle e_a, P_U e_{a'}\rangle - \tfrac{r}{n}1_{a=a'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad \Bigl|\langle e_b, P_V e_{b'}\rangle - \tfrac{r}{n}1_{b=b'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad |E_{ab}| \le \mu\tfrac{\sqrt r}{n}.$$

For a set $\Omega \subset [n]\times[n]$ of observed positions, the nuclear-norm program is

$$\text{minimize } \|X\|_* \quad \text{subject to } X_{ab} = M_{ab}\ \ ((a,b)\in\Omega). \qquad \text{(I.3)}$$

In the uniform model $\Omega$ is a uniformly random $m$-subset of $[n]\times[n]$; in the Bernoulli model each entry is included independently with probability $p = m/n^2$.

The proof works with the tangent space $T$ at $M$ and its projection $\mathcal P_T(X) = P_UX + XP_V - P_UXP_V$, the sampling projection $\mathcal P_\Omega$, and the centered operators $\mathcal Q_\Omega = p^{-1}\mathcal P_\Omega - \mathcal I$ and $\mathcal Q_T = \mathcal P_T - \rho'\mathcal I$, where $\rho = r/n$ and $\rho' = 2\rho - \rho^2$. The candidate certificate $Y$ of (III.10) is the matrix of least Frobenius norm with $\mathcal P_\Omega(Y) = Y$ and $\mathcal P_T(Y) = E$.

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

There is an absolute constant $C$ such that, for every strongly incoherent $M$ of rank $r$ and every $m \le n^2$,

$$m \ge C\mu^4 n r^2(\log n)^2 \implies \Pr_{\text{uniform}}\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.$$

Milestones

1. Lemma 3.1: a matrix $Y$ supported on $\Omega$ with $\mathcal P_T(Y) = E$ and $\|\mathcal P_{T^\perp}(Y)\| < 1$, together with injectivity of $\mathcal P_\Omega$ on $T$, certifies that $M$ is the unique solution (already proved on the platform).
2. Lemma 5.1 (exponent bound): $|J|+|K|-|Q|-|\Omega| \le -|Q'|+1$ for every admissible pair.
3. Lemma 5.2 (pair counting): at most $(Cj(k+1))^{2j(k+1)+q}$ strongly admissible pairs have $|Q'| = q$.
4. Theorem 3.4 (moment bound I): with $A = (\mathcal Q_\Omega\mathcal Q_T)^k\mathcal Q_\Omega(E)$ and $r_\mu = \mu^2 r$,

$$\mathbb E\operatorname{trace}(A^*A)^j \le (Cj(k+1))^{2j(k+1)}\, n\,(n r_\mu^2/m)^{j(k+1)}.$$

5. Corollary 3.5: under the goal's sampling condition and the Bernoulli model, with probability at least $1-n^{-3}$, $\mathcal P_\Omega$ is injective on $T$ and $\|\mathcal P_{T^\perp}(Y)\| \le 1/2$.

The Bernoulli-to-uniform transfer (at most doubling the failure probability) is already on the platform and is included as a supporting item.

Significance

Theorem 1.1 shows that a tractable convex program recovers every strongly incoherent matrix of bounded rank from $O(n(\log n)^2)$ random entries, while Theorem 1.7 of the same paper shows that no method can succeed with fewer than order $n\log n$. The gap is a single logarithmic factor. The result also requires nothing of the singular values, only of the singular vectors.

The theorem is proved in the literature, and later work improved the rank dependence (Theorem 1.2 of the same paper, and the golfing-scheme results of Gross and Recht). As far as is known, none of these results has a machine-checked proof. The mission produces a formal version of the full moment-method argument. Its combinatorial core, the admissible-pair calculus of Sections IV–V, is a self-contained counting problem for closed paths in a grid and is reusable for other trace-moment bounds of random operators. The Candès–Recht mission on the platform already supplies the deterministic duality step (Lemma 3.1) and the model transfer.

Difficulty

The obvious route bounds the Neumann series $\sum_k \|(\mathcal Q_\Omega\mathcal P_T)^k\mathcal Q_\Omega(E)\|$ term by term with noncommutative Khintchine inequalities and decoupling. That is how the earlier $n^{6/5}$ bound was obtained, and it degrades as $k$ grows because the indicator variables in the higher terms are strongly coupled. The moment method replaces these tools by an exact expansion of $\mathbb E\operatorname{trace}(A^*A)^j$ as a sum over "spider" configurations of paths in $[n]\times[n]$. The difficulty moves into combinatorics. Configurations have to be grouped by admissible pairs, the exponent of $n$ has to be matched against the powers of $1/p$ (Lemma 5.1), and the configurations have to be counted with enough precision that the sum over $q$ converges (Lemma 5.2). A naive count of pairs gives $(2j(k+1))^{4j(k+1)}$, which is too large by a square.

Formalization scope

• Square case. Theorem 1.1 is printed for $n_1\times n_2$ matrices, but the paper proves only the square case (Section I-H: "we shall work exclusively with square matrices"). Every statement is for Matrix (Fin n) (Fin n) ℝ.
• General rank. The goal and Corollary 3.5 are stated in the general-rank form (I.11), $m \ge C\mu^4 n r^2(\log n)^2$. The paper states this form explicitly on p. 2055, and the proof of Corollary 3.5 derives it as (III.26). For $r = O(1)$ it is the printed Theorem 1.1 and the printed Corollary 3.5.
• Constants. Every constant ("numerical constant $C$", $c_0$, and $O(M)^M := (CM)^M$) is an existential absolute constant quantified before $n$, $r$, $m$, $M$, $\mu$, $j$, $k$ and $q$. A constant allowed to depend on $n$ or $M$ would make (I.11) unsatisfiable for large $C$ and the goal vacuous; that formalization is ruled out.
• Standing assumptions. The paper assumes $n \ge C'$ and $m \ge 2nr$ (I.22) throughout. In the goal and in Corollary 3.5 they are absorbed by $C$, since strong incoherence forces $\mu \ge 1$. Theorem 3.4 carries $2nr \le m$ explicitly. Theorem 3.4 omits $r = O(1)$ and (I.10), since Section V uses only its own proviso $m \ge n r_\mu^2$. Every statement also carries $m \le n^2$, without which the uniform model is empty.
• Probability. The uniform model is the platform's successProb (a ratio of finite counts). The Bernoulli model uses bernoulliEventProb and bernoulliExpectation with $p = m/n^2$. The logarithm is natural, and the failure probability is written 1 / n^3.
• Recovery. "Unique solution of (I.3)" is IsUniqueMinimizer: every other matrix that agrees with $M$ on $\Omega$ has strictly larger nuclear norm. Stating recovery conditionally on the existence of a certificate would reduce the goal to Lemma 3.1; the goal instead bounds the probability of recovery itself.
• Admissible pairs. The index $i \in [j]$ is 0-based, the cyclic successor is finRotate, and the lexicographic order is compared through positions. Pair values are counted in Fin (2j(k+1)+1), which contains every admissible value, so the count is exact and finite.
• New definitions. centeredTangentProjection ($\mathcal Q_T$), momentMatrix ($A$), and the admissible-pair calculus. Strong incoherence (A1–A2) is the shared definition CandesTao.Shared.StrongIncoherence, used by this mission and by the companion mission II. The $\mathcal Q_T$ definition is drafted independently in mission II.

Contributions are welcome on any milestone. Lemmas 5.1 and 5.2 are finite combinatorics and need no analysis. Theorem 3.4 additionally needs the expansion (IV.4) of the trace moment and the moment bounds for centered Bernoulli variables of Section IV-C. Corollary 3.5 also uses Theorem 3.2 (Rudelson selection estimate) and Lemma 3.3 (replacing $\mathcal P_T$ by $\mathcal Q_T$), which are milestones of the companion mission The Power of Convex Relaxation: Near-Optimal Matrix Completion II.

Selected references

• E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
• E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9(6):717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• D. Gross, Recovering Low-Rank Matrices From Few Coefficients in Any Basis, IEEE Trans. Inf. Theory 57(3):1548–1566, 2011. https://doi.org/10.1109/TIT.2011.2104999
• B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://jmlr.org/papers/v12/recht11a.html

Motivation

A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in $\mathbb R^n$ is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.

Setting

Fix a subset $T\subseteq\mathbb R^n$. For a standard Gaussian vector $g\sim N(0,I_n)$, the Gaussian width of $T$ is $w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle$ (Chapter 7), and the stable dimension of a bounded $T$ is $d(T) := w(T)^2/\mathrm{diam}(T)^2$ up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of $T$, which can jump discontinuously under a small perturbation of $T$, unlike $d(T)$.

An $m\times n$ Gaussian random matrix with i.i.d. $N(0,1)$ entries is a random matrix $A$ each of whose $mn$ entries is an independent standard normal random variable.

Formalization targets

Goal (Theorem 11.3.3, Dvoretzky-Milman's theorem, Gaussian form)

$$\exists\,c>0:\quad m\le c\varepsilon^2 d(T) \;\Longrightarrow\; \mathbb P\bigl[(1-\varepsilon)B \subseteq \mathrm{conv}(AT) \subseteq (1+\varepsilon)B\bigr] \ge 0.99$$

for every $m\times n$ Gaussian random matrix $A$ with i.i.d. $N(0,1)$ entries, every bounded $T\subseteq\mathbb R^n$ containing the origin, and every $\varepsilon\in(0,1)$, where $B$ is the Euclidean ball of radius $w(T)$ centered at the origin. The probability $0.99$ is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.

Significance

Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every $n$-dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) $\log n$ in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube $[-1,1]^n$, for instance, is proportional to $n$ itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.

The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).

Difficulty

The natural first idea — bound $\mathrm{conv}(AT)$ directly using concentration of $\|Ax\|_2$ for each fixed $x\in T$ — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one $x$ at a time, even with a union bound over a net of $T$, does not obviously extend to the full convex hull without first controlling $\sup_{x\in T}|\langle Ax,y\rangle - w(T)\|y\|_2|$ uniformly over both $x\in T$ and $y$ on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment $(1-\varepsilon)B\subseteq\mathrm{conv}(AT)\subseteq(1+\varepsilon)B$ via a support- function duality argument (a convex body is pinned down by its support function, so bounding $\sup_{x\in T}\langle Ax,y\rangle$ uniformly over $y$ on the sphere is exactly what is needed).

Formalization scope

A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d. $N(0,1)$, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as 08-matrix-deviation). The stable dimension $d(T)$ is formalized directly as $w(T)^2/ \mathrm{diam}(T)^2$ rather than via the book's literal (but only asymptotically equivalent, per Exercise 7.6.1) definition through a squared Gaussian width $h(T-T)^2$ — the goal theorem's own proof uses only the inequality direction of that equivalence, and the goal's hypothesis already carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution preserves the theorem's exact truth content (see StableDimension's own doc-comment and MODERATION_NOTES.md for the full argument) rather than approximating it.

Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that $T$ contains the origin; its proof opens by translating $T$ so that it does ("Translating $T$ if necessary, we can assume that $T$ contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding $0\in T$ as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.

This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones should be cut rather than the goal substituted. All three are left out, not approximated, given this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup, GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions are welcome on the goal theorem itself and, beyond this mission's current scope, on the three named milestones.

Selected references

• A. Dvoretzky, Some results on convex bodies and Banach spaces, Proc. Internat. Sympos. Linear Spaces (Jerusalem, 1960), 123–160.
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 11. https://doi.org/10.1017/9781108231596