Random Matrix Theory

Motivation

Random matrices with independent rows are the workhorse of high-dimensional statistics and compressed sensing: sample covariance matrices, sub-sampled measurement operators, and randomized sketches are all of this form. A basic question about such a matrix $A$ is how close $\|Ax\|_2$ stays to its typical size $\mathbb E\|Ax\|_2\approx\sqrt m\|x\|_2$ — not just for one fixed $x$, but simultaneously for every $x$ in some set $T$ of interest (a sphere, a cone, the difference set of a data cloud). A bound that holds only pointwise in $x$ is of limited use, since most applications need to reason about the worst case over an entire geometric set at once.

This chapter proves such a uniform bound — the matrix deviation inequality — for matrices with independent, isotropic, sub-gaussian rows, controlling the deviation by a single geometric parameter of $T$, its Gaussian complexity. The result is a direct descendant of the chaining machinery of Chapter 8 (via Talagrand's comparison inequality, Chapter 8.6) and, in this book's own account, subsumes several results proved earlier by other methods — two-sided bounds on random matrices, the Johnson-Lindenstrauss lemma for infinite sets — while also yielding two new consequences central to high-dimensional convex geometry: the $M^*$ bound and the Escape theorem, both controlling how a random subspace intersects a fixed geometric set.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random vector $X$ in $\mathbb R^n$ is isotropic if its covariance matrix is the identity, $\Sigma(X)=\mathbb E[XX^\top]=I_n$ — equivalently (the book's own Lemma 3.2.3), $\mathbb E\langle X,x\rangle^2=\|x\|_2^2$ for every $x\in\mathbb R^n$. The sub-gaussian norm of a random vector $X$ is $\|X\|_{\psi_2}:=\sup_{x\in S^{n-1}}\|\langle X,x\rangle\|_{\psi_2}$, the supremum over the unit sphere of the scalar sub-gaussian (Orlicz $\psi_2$) norm of its one-dimensional marginals; $X$ is sub-gaussian when this is finite.

Fix a standard Gaussian random vector $g\sim N(0,I_n)$ in $\mathbb R^n$ (a vector whose coordinates in any orthonormal basis are independent standard normal). For a subset $T\subseteq\mathbb R^n$, the Gaussian width and Gaussian complexity of $T$ are

$$w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle, \qquad \gamma(T) := \mathbb E\sup_{x\in T}|\langle g,x\rangle|,$$

two closely related measures of the geometric size of $T$ — "cousins" that agree up to a factor of $2$ whenever $T$ contains the origin, and agree exactly when $T$ is origin-symmetric.

Formalization targets

Goal (Theorem 9.1.1, Matrix deviation inequality)

$$\exists\,C>0:\quad \mathbb E\sup_{x\in T}\bigl|\,\|Ax\|_2-\sqrt m\|x\|_2\,\bigr| \;\le\; CK^2\gamma(T)$$

for every $m\times n$ matrix $A$ whose rows $A_1,\dots,A_m$ are independent, isotropic, sub-gaussian random vectors with $K:=\max_i\|A_i\|_{\psi_2}$, and every $T\subseteq\mathbb R^n$ (whenever $\gamma(T)$ is finite). $C$ is the book's own unnamed absolute constant, hard-coded to no numeral — the weakest stable form of the claim.

Milestone (Theorem 9.4.2, the $M^*$ bound)

$$\mathbb E\,\mathrm{diam}(T\cap\ker A) \;\le\; \frac{CK^2w(T)}{\sqrt m}$$

for the same class of matrices $A$ and any bounded $T\subseteq\mathbb R^n$, where $\ker A$ is the (random) kernel of $A$, a subspace of codimension at most $m$. A direct one-paragraph consequence of the goal theorem (apply it to $T-T$, then restrict to $\ker A$, where $\|Ax-Ay\|_2$ vanishes).

Significance

The matrix deviation inequality converts a purely algebraic quantity — how close $\|Ax\|_2$ stays to $\sqrt m\|x\|_2$ — into a single geometric parameter of the index set $T$, letting it subsume, via specializations of $T$, results that were previously proved by separate ad hoc arguments: two-sided singular value bounds on random matrices ($T$ a sphere), Johnson-Lindenstrauss-type embeddings for possibly infinite point sets ($T$ a difference set), and covariance estimation. The $M^*$ bound is one of the two classical consequences the book develops fresh from the inequality (the other, the Escape theorem, is outside this mission's scope): it answers, quantitatively, how large a random affine section of a fixed convex body typically is, a question at the heart of the local theory of Banach spaces and of compressed sensing's recovery guarantees (Chapter 10 builds directly on this chapter's machinery). Both results have long-standing, well-understood classical proofs; this mission formalizes their statements, not open research.

Difficulty

The natural first idea — bound $\|Ax\|_2-\sqrt m\|x\|_2$ pointwise for a fixed $x$ using concentration of the norm of a sub-gaussian random vector, then take a union bound over $T$ — only works when $T$ is finite, and gives a bound that scales with $\log|T|$ rather than with the actual geometric size of $T$. The book's actual route treats $X_x:=\|Ax\|_2-\sqrt m\|x\|_2$, indexed by $x\in\mathbb R^n$, as a genuine random process and shows it has sub-gaussian increments ($\|X_x-X_y\|_{\psi_2}\le CK^2\|x-y\|_2$) — itself a nontrivial fact proved in stages (first for a single unit vector via concentration of the norm, Theorem 3.1.1; then for a pair of unit vectors via a squared-process argument; only then in full generality) — and then invokes Talagrand's comparison inequality (a consequence of the chaining machinery of Chapter 8) to pass from sub-gaussian increments directly to a bound in terms of Gaussian complexity, without ever performing a union bound over $T$ itself.

Formalization scope

A is represented by its rows, A : Fin m → Ω → EuclideanSpace ℝ (Fin n), with ‖Ax‖₂ recovered as Real.sqrt (∑ i, ⟨Aᵢ,x⟩²) rather than constructing A as a Matrix/LinearMap — this matches the book's own row-by-row hypotheses exactly and is what both theorems' own proofs use directly. IsIsotropic is formalized via the book's basis-free Lemma 3.2.3 characterization (E⟨X,x⟩² = ‖x‖² for every x) rather than the matrix equation Σ(X)=Iₙ, avoiding a fixed-basis covariance-matrix construction the rest of this chunk's definitions do not otherwise need. SubgaussianVectorNorm reuses the published scalar subgaussianNorm. GaussianWidth and GaussianComplexity realize the standard Gaussian vector g ∼ N(0,Iₙ) as the identity map on Mathlib's own standard Gaussian measure on a finite-dimensional inner product space (ProbabilityTheory.stdGaussian), and both, together with the goal's own left-hand side, use a locally-defined finite-marginal expected-supremum convention (ExpSup, EReal-valued) matching the book's own footnote-3 convention (Section 7.2), reused throughout the series. Both theorems' right-hand sides presuppose their respective geometric parameter ($\gamma(T)$ or $w(T)$) is a finite real number; since both are EReal-valued in general, each theorem takes an explicit real witness together with a proof that it equals the true value — the same finiteness-disclosure pattern 07-chaining's Dudley inequality uses for its own right-hand integral, needed here for exactly the same reason (the book's own display does not spell out why the quantity is finite, true whenever $T$ is bounded, as in every application). $C$ (and, in the milestone, the same $C$ again — the two are not asserted equal, matching that the book states them as two separate "absolute constants") is existentially quantified before every type, instance and hypothesis it is uniform over. The $M^*$ bound milestone (m_star_bound) additionally carries the hypothesis $m > 0$: its conclusion divides by $\sqrt m$, and without this hypothesis Lean's real-division convention ($x/0=0$) makes the right-hand side $0$ at $m=0$ regardless of $C, K, w(T)$ — false whenever $T$ has positive diameter, not merely a weaker or vacuous claim. The book's own proof ("Dividing by $\sqrt m$ yields …", p. 241) already implicitly assumes $m \ge 1$, matching every other use of $m$ in the chapter as a positive count of measurement rows.

A trivializing formalization would fix $T$ to be a finite set, collapsing the goal to the elementary union-bound case the book explicitly contrasts its own more general statement against (Section 9.1's opening paragraph: "we may choose an arbitrary subset $T\subseteq\mathbb R^n$"); this mission's goal quantifies over an arbitrary Set (EuclideanSpace ℝ (Fin n)) to rule that out.

This mission covers Theorem 9.1.1 and Theorem 9.4.2 only; Theorem 9.4.7 (the Escape theorem) and Theorem 9.2.4 (covariance estimation for lower-dimensional distributions), both named as candidate milestones, are left out for lack of session time given the substantial shared infrastructure this chapter needed from scratch. ExpSup, IsIsotropic, SubgaussianVectorNorm, GaussianWidth and GaussianComplexity are reusable by any later chapter needing an isotropic or sub-gaussian random vector, or a Gaussian-width-type quantity (Chapters 4, 10, 11 of this same book series all use one or more of these notions). Solvers' contributions are welcome on: Theorem 9.1.3 (the sub-gaussian increments of the deviation process, the technical heart of the goal's proof), Talagrand's comparison inequality itself (outside this mission, in 07-chaining's companion chapter), and the one-paragraph reduction from the goal to the $M^*$ bound.

Selected references

• S. Mendelson, A. Pajor, N. Tomczak-Jaegermann, Reconstruction and subgaussian operators in asymptotic geometric analysis, Geometric and Functional Analysis 17 (2007), 1248–1282. https://doi.org/10.1007/s00039-007-0618-7
• 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 9. https://doi.org/10.1017/9781108231596

Motivation

Matrix approximation replaces a large or complicated matrix with a random matrix that is easier to store or compute. Averaging independent realizations improves accuracy while retaining the structure of each realization. Examples in Tropp's monograph include sparse approximations and randomized matrix products. The practical question is how the number of samples, the size of one sample, and its second moment control the spectral norm error. Tropp, §6.2

The book proves a matrix Bernstein inequality in Theorem 6.1.1, then applies it to an empirical matrix average in Corollary 6.2.1. Theorem 6.1.1 is already posed as TroppMatrixConcentration.matrix_bernstein on Prove2Me and is currently Open. This mission records the application with its own hypotheses and constants. The capstone concerns the estimator that a reader would construct, rather than a sum of abstract centered summands. Tropp, §§6.1–6.2

Setting

Let $B$ be a fixed complex $d_1\times d_2$ matrix. A sample matrix $R$ has the same size, has expectation $B$, and has spectral norm at most $L$ almost surely. The equality $\mathbb ER=B$ makes one sample an unbiased estimate of $B$. The almost-sure bound limits the size of every sample except on a probability-zero set. The dimensions $d_1,d_2$ are positive integers, and $n$ is a positive sample count.

Take independent copies $R_1,\ldots,R_n$ with the distribution of $R$. Their matrix sampling estimator is

$$\overline R_n=\frac1n\sum_{k=1}^nR_k.$$

For any rectangular matrix $A$, $A^*$ denotes its conjugate transpose and $\|A\|$ its spectral norm. The per-sample second moment is

$$m_2(R)=\max\{\|\mathbb E(RR^*)\|,\|\mathbb E(R^*R)\|\}.$$

Both terms matter for a rectangular matrix: $RR^*$ and $R^*R$ act on different coordinate spaces. All expectations of matrices are entrywise expectations, represented by Bochner integrals in Lean. The almost-sure norm bound guarantees the moments used here are finite. Tropp, equations (6.2.4)–(6.2.6)

Formalization targets

Empirical matrix approximation

Corollary 6.2.1 gives an expectation estimate and a tail estimate for the same estimator. For every real $t\ge0$,

$$\mathbb E\|\overline R_n-B\|\le \sqrt{\frac{2m_2(R)\log(d_1+d_2)}{n}}+ \frac{2L\log(d_1+d_2)}{3n},$$ $$\mathbb P\{\|\overline R_n-B\|\ge t\}\le (d_1+d_2)\exp\left(\frac{-nt^2/2}{m_2(R)+2Lt/3}\right).$$

The goal includes both bounds. The expectation estimate controls average error; the tail estimate controls the chance of an error above a chosen threshold. The dimension enters only through $\log(d_1+d_2)$ in the expectation bound and the factor $d_1+d_2$ in the tail bound. These are the book's constants, including the factors $2$ and $3$ in the linear terms. Tropp, Corollary 6.2.1, p. 81

Supporting statements

The milestone list follows Corollary 6.1.2 for uncentered summands, the bound $\|n^{-1}(R_k-B)\|\le2L/n$, and the variance estimate $v(\overline R_n-B)\le m_2(R)/n$. Equation (6.2.7) is a companion: a stated lower bound on $n$ implies $\mathbb E\|\overline R_n-B\|\le2\varepsilon$ for $\varepsilon>0$. Tropp, pp. 77, 82

Significance

The result turns a bound on one random matrix into a quantitative guarantee for an empirical approximation. It lets a user choose a sample count for a target error and evaluate both average error and failure probability. The same framework is instantiated later in the monograph for matrix sparsification and multiplication; those applications depend on controlling $L$ and $m_2(R)$ for their particular sampling laws. Tropp, §§6.2–6.4

This is a known mathematical result proved in the book. Its Lean statement is an open formalization target. The mission adds a reusable empirical-mean definition and application statements built on the already published matrix spectral norm and rectangular second-moment definitions. A proof of the general matrix Bernstein theorem remains separate; the mission can draw on it when that platform theorem is proved.

Difficulty

The estimator error is a centered sum, but the sampling assumptions are given for an uncentered random matrix $R$. Bounding the centered summands changes the uniform bound from $L$ to $2L/n$. The variance parameter must be related to the second moment of one uncentered sample, with the correct $1/n$ scaling. Dropping the common-distribution condition would leave no relation between the samples' second moments and $m_2(R)$. Applying scalar concentration to entries would not directly give the stated spectral norm bound or its dimension dependence. Tropp, proof of Corollary 6.2.1, p. 82

Formalization scope

Matrices are Matrix (Fin d₁) (Fin d₂) ℂ. The spectral norm and rectSecondMoment are imported from tc's published TroppMatrixConcentration definitions. An arbitrary probability space carries a measurable reference matrix $R_0$ and a finite family $R_k$; iIndepFun expresses independence and IdentDistrib expresses equality in law with $R_0$. The estimator is the finite sum scaled by $n^{-1}$. No particular sampling scheme or deterministic choice of $R$ is fixed: the formal goal requires only the source's unbiasedness and boundedness conditions.

The Lean statements explicitly require $d_1,d_2\ge1$, $n>0$, measurability, and the almost-sure form of $\|R\|\le L$. These make the logarithm and inverse sample count meaningful and make the random matrix laws well behaved. For the uncentered Bernstein corollary, integrability of each $S_k$ is explicit because a bounded deviation from an unspecified mean alone does not establish that the mean exists. The goal also asserts integrability of its error norm, preventing a Bochner integral from silently taking Lean's default value for a nonintegrable function. The bound on $R$ supplies that integrability. When the denominator in a tail formula is zero, the displayed total real division gives a loose bound at the degenerate case; the source's probabilistic claim remains valid.

Contributions that formalize the centered-summand calculation, the variance estimate, or the transfer from the general matrix Bernstein theorem are within scope. The imported matrix and probability definitions are reusable in other matrix concentration missions. The local empirical-mean definition is reusable whenever a matrix estimator averages finitely many random samples.

Selected references

• Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, especially §§6.1–6.4.

Motivation

Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.

Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.

Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.

Setting

All matrices are $d\times d$ with complex entries, $d\ge 1$. A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. $A$, $\lambda_{\max}(A)$ is its largest eigenvalue and $\|A\|$ its spectral norm. Functions of s.a. matrices are defined spectrally: if $A=Q\Lambda Q^*$ then $e^{A}=Qe^{\Lambda}Q^*$, and $\log$ is defined the same way on positive-definite matrices. $A\preceq B$ is the semidefinite order: $B-A$ is positive semidefinite.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $\mathcal F_0\subset\mathcal F_1\subset\cdots\subset\mathcal F$, and write $\mathbb E_k[\,\cdot\,]=\mathbb E[\,\cdot\mid\mathcal F_k]$. The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence $X_1,\dots,X_n$ of random matrices is adapted when each $X_k$ is $\mathcal F_k$-measurable. A matrix martingale is an adapted sequence of s.a. matrices $Y_k$ with $\mathbb E\|Y_k\|<\infty$ and $\mathbb E_{k-1}Y_k=Y_{k-1}$; its difference sequence $X_k=Y_k-Y_{k-1}$ satisfies $\mathbb E_{k-1}X_k=0$.

The hypotheses of the main theorem are: $X_1,\dots,X_n$ is an adapted sequence of random s.a. matrices, and $A_1,\dots,A_n$ is a fixed (non-random) sequence of s.a. matrices, with

$$\mathbb E_{k-1}X_k = 0 \qquad\text{and}\qquad X_k^2\preceq A_k^2\ \text{ almost surely.}$$

The variance parameter is $\sigma^2 := \big\|\sum_k A_k^2\big\|$.

Formalization targets

Goal: Theorem 7.1 (Matrix Azuma), p. 27

For all $t\ge 0$,

$$\mathbb P\Big\{\lambda_{\max}\Big(\sum_{k}X_k\Big)\ge t\Big\}\le d\cdot e^{-t^2/8\sigma^2}.$$

Milestones

In the order they are used:

1. Display (2.6), Golden–Thompson: $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ for s.a. $A,H$.
2. Proposition 3.1, the Laplace transform method: $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}$.
3. Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E e^{X})$.
4. Lemma 4.3, Rademacher half: $\mathbb E e^{\varepsilon\theta A}\preceq e^{\theta^2A^2/2}$.
5. Lemma 7.6 (Symmetrization): $\mathbb E\operatorname{tr}e^{H+X}\le\mathbb E\operatorname{tr}e^{H+2\varepsilon X}$ when $\mathbb EX=0$ and $\varepsilon$ is an independent Rademacher variable.
6. Lemma 7.7 (Azuma cgf): $\log\mathbb E[e^{2\varepsilon\theta X}\mid X]\preceq2\theta^2A^2$ when $X^2\preceq A^2$.
7. Display (7.5): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(2\theta^2\sum_kA_k^2)$ under the hypotheses of the goal.

Further statements

Corollary 7.2 is the martingale form, $\mathbb P\{\lambda_{\max}(Y_n-\mathbb EY_n)\ge t\}\le d\,e^{-t^2/8\sigma^2}$. Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, $\mathbb P\{\lambda_{\max}(H(z)-\mathbb EH(z))\ge t\}\le d\,e^{-t^2/8\sigma^2}$ for a matrix-valued function $H$ of independent variables whose changes in one coordinate $k$ have squares bounded by $A_k^2$.

Significance

The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor $d$, and a variance parameter equal to the norm of the sum $\sum_kA_k^2$ rather than the sum of the norms $\sum_k\|A_k\|^2$. In the commuting case the two coincide; in general the first can be smaller by a factor of up to $n$. The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).

Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.

Difficulty

The scalar proof of Azuma's inequality multiplies conditional moment generating functions, $\mathbb E e^{\theta\sum X_k}=\mathbb E\big[e^{\theta\sum_{k<n}X_k}\,\mathbb E_{n-1}e^{\theta X_n}\big]$, and bounds each factor. For matrices this fails: $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, and $\operatorname{tr}e^{A+B+C}\le\operatorname{tr}(e^Ae^Be^C)$ is false, so the Golden–Thompson inequality cannot be iterated over $n$ terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis $X_k^2\preceq A_k^2$ bounds squares, not the matrices themselves; it does not give $X_k\preceq A_k$, so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and $\preceq$ is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. $\lambda_{\max}$ is the supremum of the real spectrum, which is why $d\ge1$ is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by $k=1,\dots,n$, so $\mathcal F_{k-1}$ is never truncated. The bound $X_k^2\preceq A_k^2$ is required almost surely. The bounds $A_k$ are deterministic matrices. The infimum over $\theta>0$ in Proposition 3.1 is posed as the bound for each $\theta>0$ at which the expectation is finite.

The hypotheses must not be made vacuous. Integrability of each $X_k$ is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is $0$ and the centring hypothesis would say nothing. The $X_k$ are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.

Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given $X$ is replaced by the expectation over $\varepsilon$ at each fixed value $x$ with $x^2\preceq A^2$; by independence these agree. Corollary 7.2 adds the hypothesis that $Y_0$ is almost surely constant, without which $Y_n-\mathbb EY_n\neq\sum_kX_k$.

A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited version arXiv:1004.4389v7 (2011). https://arxiv.org/abs/1004.4389v7
• R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
• J. A. Tropp, Freedman's inequality for matrix martingales, Electron. Commun. Probab. 16 (2011) 262–270. https://arxiv.org/abs/1101.3039
• R. I. Oliveira, Concentration of the adjacency matrix and of the Laplacian in random graphs with independent edges, arXiv:0911.0600 (2010). https://arxiv.org/abs/0911.0600
• C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer (1998) 195–248. https://doi.org/10.1007/978-3-662-12788-9_6
• R. Bhatia, Matrix Analysis, Springer GTM 169 (1997), Sec. IX.3. https://doi.org/10.1007/978-1-4612-0653-8
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X

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

A partially observed array with three indices appears when data record relationships among triples of objects. If its entries have a low-rank structure, one can hope to recover the full array from far fewer than $d^3$ measurements. Cai, Li, Poor and Chen study this problem when the measurements are noisy and only a random subset of entries is seen. Their result gives a statistical error bound for a concrete two-stage method: spectral initialization followed by ordinary gradient descent on a nonconvex loss. It is a known theorem, proved in the pinned preprint, rather than an open conjecture.

Setting

The unknown symmetric order-three tensor is $T^\star\in\mathbb R^{d\times d\times d}$. It has a CP decomposition $T^\star=\sum_{s=1}^r(u_s^\star)^{\otimes3}$, where the nonzero columns $u_s^\star$ form $U^\star\in\mathbb R^{d\times r}$. Each unordered triple of coordinates is sampled independently with probability $p$; its six permutations share one sampling decision. On a sampled triple the observation is $T^\star_{ijk}+E_{ijk}$, with symmetric, centered, independent sub-Gaussian noise of variance at most $\sigma^2$. The observed tensor $T$ vanishes outside the sampled set $\Omega$.

For a candidate factor matrix $U=[u_1,\ldots,u_r]$, the objective is

$$f(U)=\frac{1}{6p}\left\|P_\Omega\!\left(\sum_{s=1}^r u_s^{\otimes3}-T\right)\right\|_F^2.$$

Algorithm 2 obtains a leading $r$-dimensional eigenspace from an off-diagonal Gram matrix of the mode-one unfolding of $p^{-1}T$. Algorithm 3 uses Gaussian restarts, leading singular vectors, and greedy pruning to turn that subspace into a factor matrix $U^0$. Algorithm 1 then applies the gradient step to $f$. Eigenvalue ties, leading singular-vector choices, and pruning ties can produce several admissible executions; the result concerns every execution.

Incoherence $\mu$ measures how evenly the tensor and factors spread across coordinates and how nearly orthogonal distinct factors are. The condition number $\kappa$ is the ratio of the largest to smallest factor norm. Write $\lambda^\star_{\min}=\min_s\|u_s^\star\|_2^3$ and $\lambda^\star_{\max}=\max_s\|u_s^\star\|_2^3$. Distances $\operatorname{dist}_F$, $\operatorname{dist}_\infty$, and $\operatorname{dist}_{2,\infty}$ minimize their respective matrix norms over permutations of the $r$ columns.

Formalization targets

The goal is Theorem 2.4, in the bounded-rank, bounded-incoherence, bounded-condition-number regime. Under its printed sampling, noise, restart, threshold and step-size conditions, for every $0\le t\le d^5$ it asserts, with probability at least $1-\delta$,

$$\operatorname{dist}_F(U^t,U^\star)\le\left(C_1\rho^t+C_2\frac{\sigma}{\lambda^\star_{\min}}\sqrt{\frac{d\log d}{p}}\right)\|U^\star\|_F,$$ $$\operatorname{dist}_\infty(U^t,U^\star)\le\operatorname{dist}_{2,\infty}(U^t,U^\star)\le\left(C_3\rho^t+C_4\frac{\sigma}{\lambda^\star_{\min}}\sqrt{\frac{d\log d}{p}}\right)\|U^\star\|_{2,\infty}.$$

The rate is fixed to $\rho=1-\lambda_{\min}^{\star,4/3}\eta/5$, consistent with the paper's local-convergence lemmas. Milestones formalize the gradient identity (36), local Hessian bounds (Lemma 5.1), spectral-subspace recovery (Lemma 5.7), factor retrieval (Theorem 5.9), and the paper's general-parameter recovery theorem (Theorem 2.8). The latter makes the dependence on $\mu$ and $r$ explicit.

Significance

The inequalities give two guarantees at once: geometric reduction of initialization error and an explicit noise floor. The $2,\infty$ bound controls the error in each coordinate row, which a Frobenius estimate alone does not supply. Together with the tensor-entry corollaries in the paper, they explain the accuracy of this practical nonconvex method under random subsampling. The authors also specify how the sample probability, noise level, rank and incoherence interact, so the result can be compared to other tensor-completion methods.

This mission asks for a machine-checked version of the known result. Its published ψ₂ norm definition is reused; the paper-specific tensor model, spectral initialization relations, loss and gradient iteration are new. The theorem statements compile with sorry, so none of their proofs is claimed as machine checked here. Proofs of the listed milestones, the main theorem, and faithful auxiliary concentration results are welcome; the paper's numerical experiments are outside this formalization.

Difficulty

The gradient loss is nonconvex, so global convexity cannot justify the iteration bound. The local Hessian estimate applies only near $U^\star$ in both Frobenius and rowwise norm. A Frobenius estimate alone cannot establish the rowwise condition at every iteration. The spectral initializer must also select individual factors from a subspace despite nearly tied eigenvalues and noisy tensor contractions. These are the points where a direct appeal to standard smooth-gradient-descent theory stops short of the stated result.

Formalization scope

Coordinates are Fin d and Fin r, with zero-based indexing; the PDF uses one-based indices. All logarithms are natural. Tensor and matrix norms are explicit finite-coordinate Euclidean norms. Minima over permutations range over all permutations of Fin r, and maxima in the incoherence parameters range over the indices specified by Definition 2.1. Sampling is on sorted triples, then extended by symmetry. The probability model is a single probability space carrying the sampling indicators, noise variables and Gaussian restarts, jointly independent; the paper leaves some cross-family independence implicit. Noise has mean zero, variance at most $\sigma^2$, and ψ₂ norm at most $\sigma$ using the published extended-nonnegative norm. The last bound makes the paper's sub-Gaussian scale explicit.

The statements use $d\ge d_0\ge2$, $r\ge1$, nonzero true factor columns, $0<p\le1$, and $\sigma\ge0$. Theorems 2.8 and 5.9 use $r\ge2$ and round their real-valued restart count up to a natural number; this handles the boundary where $\log r=0$. Theorem 2.4 places its claimed absolute error constants before the rank and incoherence bounds and all instance data. Probability is expressed as the outer measure of the bad event, since admissible-execution predicates quantify over choices and need not be measurable. Each good event explicitly asserts that an admissible execution exists before requiring the bounds for every execution; otherwise a failed pruning run would make a universal claim vacuous.

The remaining reusable infrastructure includes concentration for symmetric sampled tensors, finite-dimensional spectral perturbation with ties, and derivative estimates for the cubic factor map. The paper's leave-one-out iteration lemmas and their auxiliary estimators are not included in this initial milestone list; they remain natural contributions toward the full proof.

Selected references

• C. Cai, G. Li, H. V. Poor and Y. Chen, Nonconvex Low-Rank Tensor Completion from Noisy Data, arXiv:1911.04436v2, 2021; published in Operations Research 70(2), 2022. Preprint.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Definition 2.5.6 for the ψ₂ norm. Publisher DOI.

Motivation

Matrix completion asks for a low-rank matrix from a small random subset of its entries. It models collaborative filtering (recommendation systems), sensor-network localisation, and structure from motion. In practice the revealed entries are corrupted by noise, and the most widely used estimator is nuclear-norm regularized least squares: fit the observed entries in squared error while penalizing the sum of singular values. The estimator is a convex program, so it is solved reliably by proximal and singular-value-thresholding methods, and it needs no knowledge of the rank.

Its statistical accuracy was not understood. In the noiseless case, convex relaxation recovers the matrix exactly from nearly the information-theoretic minimum number of samples (Candès–Recht 2009, Candès–Tao 2010, Gross 2011). With noise, the available bounds for the plain convex program (Candès–Plan 2010) give $\|Z_{\rm cvx}-M^\star\|_F\lesssim\sigma n^{3/2}$ under random noise. That can be a factor of order $\sqrt{n^2p}$ above the oracle lower bound, and the numerical performance of the program is far better. Sharper rates were known only for modified estimators: Negahban–Wainwright 2012 add a spikiness constraint, Koltchinskii–Lounici–Tsybakov 2011 use a different estimator. In 2019, Chen, Chi, Fan, Ma and Yan (arXiv:1902.07698; SIAM J. Optim. 30(4), 2020, doi:10.1137/19M1290000) showed that the unmodified convex program attains near-optimal error in the Frobenius, entrywise and spectral norms simultaneously. Their argument goes through nonconvex gradient descent. This mission formalizes that theorem.

Setting

The unknown matrix is $M^\star\in\mathbb R^{n\times n}$ of rank $r\ge1$, with singular value decomposition $M^\star=U^\star\Sigma^\star V^{\star\top}$. The columns of $U^\star,V^\star\in\mathbb R^{n\times r}$ are orthonormal, and $\Sigma^\star=\mathrm{diag}(\sigma^\star_1,\dots,\sigma^\star_r)$ with $\sigma_{\max}=\max_k\sigma^\star_k$, $\sigma_{\min}=\min_k\sigma^\star_k>0$ and condition number $\kappa=\sigma_{\max}/\sigma_{\min}$. Write $\|A\|_{2,\infty}$ for the largest Euclidean norm of a row of $A$. $M^\star$ is $\mu$-incoherent if $\|U^\star\|_{2,\infty}\le\sqrt{\mu r/n}$ and $\|V^\star\|_{2,\infty}\le\sqrt{\mu r/n}$ (Definition 1). Incoherence says that the energy of $M^\star$ is not concentrated on a few rows or columns.

Under Assumption 1, each index $(i,j)$ enters the observed set $\Omega$ independently with probability $p$. One observes $M_{ij}=M^\star_{ij}+E_{ij}$ for $(i,j)\in\Omega$, where the $E_{ij}$ are i.i.d., zero-mean, and have sub-Gaussian norm $\|E_{ij}\|_{\psi_2}=\sup_{q\ge1}q^{-1/2}(\mathbb E|E_{ij}|^q)^{1/q}\le\sigma$. Let $\mathcal P_\Omega$ keep the entries indexed by $\Omega$ and zero the rest. The convex estimator is any minimizer $Z_{\rm cvx}$ of

$$g(Z)=\tfrac12\|\mathcal P_\Omega(Z-M)\|_F^2+\lambda\|Z\|_*,\qquad\lambda=C_\lambda\sigma\sqrt{np},\qquad(3)$$

where $\|Z\|_*$ is the nuclear norm, $\|\cdot\|$ is the spectral norm and $\|\cdot\|_\infty$ is the largest absolute entry.

Formalization targets

Goal: Theorem 2

Suppose $n^2p\ge C\kappa^4\mu^2r^2n\log^3n$ and $\sigma\sqrt{n/p}\le c\,\sigma_{\min}/\sqrt{\kappa^4\mu r\log n}$. Then with probability $1-O(n^{-3})$, every minimizer of (3) satisfies

$$\|Z_{\rm cvx}-M^\star\|_F\lesssim\kappa\tfrac{\sigma}{\sigma_{\min}}\sqrt{\tfrac np}\|M^\star\|_F,\quad\|Z_{\rm cvx}-M^\star\|_\infty\lesssim\sqrt{\kappa^3\mu r}\tfrac{\sigma}{\sigma_{\min}}\sqrt{\tfrac{n\log n}p}\|M^\star\|_\infty,\quad\|Z_{\rm cvx}-M^\star\|\lesssim\tfrac{\sigma}{\sigma_{\min}}\sqrt{\tfrac np}\|M^\star\|.$$

Every best rank-$r$ approximation $Z_{{\rm cvx},r}$ is within $n^{-3}\frac\sigma{\sigma_{\min}}\sqrt{n/p}\,\|M^\star\|$ of $Z_{\rm cvx}$ in Frobenius norm, and satisfies the same three bounds.

Milestones

1. Deterministic layer: Lemma 20 (balancing an SVD factorization), Claim 3, Claim 2 and Lemma 2. Lemma 2 says that a point $(X,Y)$ with $\|\nabla f(X,Y)\|_F\le c\frac{\sqrt{c_{\rm inj}p}}{\kappa}\frac\lambda p\sqrt{\sigma_{\min}}$ for the factored objective

$$f(X,Y)=\tfrac1{2p}\|\mathcal P_\Omega(XY^\top-M)\|_F^2+\tfrac\lambda{2p}(\|X\|_F^2+\|Y\|_F^2)$$

satisfies $\|XY^\top-Z_{\rm cvx}\|_F\le2304\,\frac{\kappa}{c_{\rm inj}\sqrt{\sigma_{\min}}}\|\nabla f(X,Y)\|_F$ under Conditions 1–2. 2. Probabilistic layer: Lemma 3 (Condition 1(a)), Lemma 19, Lemmas 7 and 8, and Lemma 4. Lemma 4 gives Conditions 1(b) and 2 uniformly over an $\ell_{2,\infty}$ neighbourhood of the truth. 3. Algorithmic layer: Lemma 5, the error bounds and the small-gradient iterate of gradient descent started at the truth, and (31), its consequence for $X^tY^{t\top}-M^\star$.

Significance

The bounds of Theorem 2 match the minimax lower bounds up to logarithmic factors when $r$ and $\kappa$ are bounded. This holds in all three norms and for noise of any size below a threshold. The theorem also shows that the convex solution is nearly of rank $r$. Neither statement requires modifying the estimator, so practitioners running standard solvers get the guarantee as is. The entrywise bound (11b) shows an implicit regularization: the convex program spreads its error over all entries without being told to.

The theorem has a complete published proof. What this mission adds is a machine-checked version, which has value of its own here. The proof chains about twenty lemmas, including a leave-one-out analysis of gradient descent with polynomially many iterations. Its constants are hidden behind "$\lesssim$" at nearly every step. The formal development fixes the quantifier order of every such constant. It also records the hypotheses the proof uses without stating them, such as the independence of the sampling pattern from the noise. No part of this paper has been formalized before. The deterministic layer (Lemmas 20, 2, Claims 2–3) applies to any Burer–Monteiro factorization of a nuclear-norm problem, not only to this one.

Difficulty

The obvious approach is to analyse the convex program directly through a dual certificate, as in the noiseless theory. With noise there is no exact recovery, and the certificate approach loses a factor polynomial in $n$. The difficulty is to transfer statistical bounds from a point one can control, the nonconvex iterate, to a point one cannot construct, the convex minimizer. The two are compared through an approximate first-order condition. That comparison is useful only if injectivity and concentration hold uniformly over all factor pairs near the truth, because the iterates depend on $\Omega$ and on the noise. A fixed-tangent-space injectivity bound, the usual tool, does not suffice. The entrywise control of the iterates requires leave-one-out sequences, and those sequences make up most of the appendix.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ and factors Matrix (Fin n) (Fin r) ℝ, using the published matrix_completion_basic, _svd and _tangent definitions (nuclear norm, SVD data, $\mathcal P_\Omega$, $\mathcal P_T$, spectral, Frobenius and entrywise norms). $M^\star$ comes with an explicit SVD with $r\ge1$ positive singular values, so its rank is exactly $r$. Definition 1 is MatrixCompletion.A0. The sub-Gaussian bound is the moment form of [Ver12, Definition 5.7] above, not Mathlib's MGF form. The randomness lives on an arbitrary probability space. The sampling indicators and the noise entries are each mutually independent, and the two families are independent of each other. This last independence is an added hypothesis, which the paper's proofs use. "With probability $1-O(n^{-k})$" is stated as an outer-measure bound $C_{\rm fail}n^{-k}$ on the failure event. Every unnamed constant ("$\lesssim$", "sufficiently large $C$", "sufficiently small $c$") is an existential placed before $n$ and all data, together with an $n_0$. Explicit constants of the paper are kept: the exponents $-3$ and $-10$, $\lambda/8$, $1/(32\kappa)$, $72\kappa$, $8\sqrt\kappa$, $t_0=n^{18}$, $n^{-5}$, the factors $3$ in (31), the $1/n^3$ in (12), and $2304=32\cdot72$ in Lemma 2.

The goal keeps the randomness in the statement. A version with fixed $\Omega$ and $E$ that assumes Conditions 1–2 or the conclusions of Lemma 5 would be Lemma 2 plus (31), not Theorem 2, and is not acceptable as a proof of the goal. The goal quantifies over every minimizer of (3) and every best rank-$r$ approximation. Excluded: Theorem 1 (the $r,\kappa=O(1)$ corollary), the noise condition of Remark 4, approximate minimizers (Remark 6), Lemmas 1 and 6, and the internal lemmas of the leave-one-out analysis (App. D), which solvers may add as supporting theorems. The development needs nuclear-norm subgradients, Weyl's inequality, matrix Bernstein and spectral-norm bounds for sparse random matrices. These are reusable well beyond this mission, and contributions of them are welcome. Theorem and equation numbers are those of the authors' preprint (Sep. 2019, arXiv:1902.07698) and may differ in the SIAM typesetting.

Selected references

• Y. Chen, Y. Chi, J. Fan, C. Ma, Y. Yan, Noisy Matrix Completion: Understanding Statistical Guarantees for Convex Relaxation via Nonconvex Optimization, SIAM J. Optim. 30(4), 2020. https://doi.org/10.1137/19M1290000 (preprint: https://arxiv.org/abs/1902.07698)
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9, 2009. https://doi.org/10.1007/s10208-009-9045-5
• E. J. Candès, Y. Plan, Matrix Completion With Noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722
• S. Negahban, M. J. Wainwright, Restricted strong convexity and weighted matrix completion: optimal bounds with noise, J. Mach. Learn. Res. 13, 2012. https://jmlr.org/papers/v13/negahban12a.html
• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011. https://doi.org/10.1214/11-AOS894
• C. Ma, K. Wang, Y. Chi, Y. Chen, Implicit Regularization in Nonconvex Statistical Estimation, Found. Comput. Math. 20, 2020. https://doi.org/10.1007/s10208-019-09429-9
• R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, CUP, 2012. https://arxiv.org/abs/1011.3027

Motivation

Approximate message passing (AMP) is a family of iterative algorithms driven by a large random matrix. It was introduced for compressed sensing by Donoho, Maleki and Montanari (PNAS 2009), and it is also used for low-rank matrix estimation, regression and spin-glass optimization. Its main appeal is that, for Gaussian random matrices, the empirical distribution of its iterates is tracked exactly in the large-dimensional limit by a scalar or low-dimensional recursion called state evolution. Bolthausen (CMP 2014) and Bayati and Montanari (IEEE Trans. Inf. Theory 2011) proved this for Gaussian matrices. Those proofs condition on the matrix through linear observations, and that conditioning argument works only for Gaussian entries.

In practice, and in the compressed-sensing phase transition that motivates the paper, the matrices are not Gaussian: Bernoulli, Rademacher and other sub-Gaussian ensembles are used. Bayati, Lelarge and Montanari (arXiv:1207.7321, Ann. Appl. Probab. 25(2), 2015) prove that the asymptotic behaviour of AMP with polynomial nonlinearities is universal: it depends on the law of the matrix entries only through their variances. This mission formalizes that universality theorem, Theorem 3 of the paper, together with the main steps of its proof.

Setting

Fix a dimension $q \ge 1$ and a degree bound $d \ge 0$. For each $N$, an AMP instance consists of three objects:

• a symmetric matrix $A \in \mathbb R^{N\times N}$ with $A_{ii} = 0$;
• polynomial maps $f^j(\cdot\,; t):\mathbb R^q\to\mathbb R^q$ of degree at most $d$, one for each $j\in[N]$ and each time $t\ge 0$;
• an initial condition $x^0 = (x^0_1,\dots,x^0_N)$ with $x^0_i \in \mathbb R^q$.

The AMP orbit is

$$x^{t+1}_i \;=\; \sum_{j} A_{ij}\, f^j(x^t_j; t) \;-\; \sum_{j} A_{ij}^2\, \frac{\partial f^j}{\partial x}(x^t_j; t)\, f^i(x^{t-1}_i; t-1),$$

where $\partial f^j/\partial x$ is the $q\times q$ Jacobian. The second term, the memory or Onsager term, is absent at $t=0$. A sequence of random instances indexed by $N$ is $(C,d)$-regular if it satisfies the following conditions:

1. the entries $A_{ij}$, $i<j$, are independent and centered, and each is sub-Gaussian with scale factor $C/N$, that is, $\mathbb E e^{\lambda A_{ij}}\le e^{C\lambda^2/(2N)}$ for all real $\lambda$;
2. all coefficients of the polynomials are bounded by $C$;
3. the matrix, the polynomials and the initial condition are mutually independent;
4. $\sum_i \exp(\|x^0_i\|_2^2/C)\le NC$.

The proof also uses an auxiliary message-passing iteration. It consists of messages $z^t_{i\to j}\in\mathbb R^q$ with $z^0_{i\to j}=x^0_i$ and

$$z^{t+1}_{i\to j}(r)=\sum_{\ell\neq j} A_{\ell i}\, f^\ell_r(z^t_{\ell\to i};t),\qquad z^{t+1}_{i}(r)=\sum_{\ell} A_{\ell i}\, f^\ell_r(z^t_{\ell\to i};t).$$

Monomials are written $x^m=\prod_r x(r)^{m(r)}$ for $m\in\mathbb N^q$.

Formalization targets

Goal: Theorem 3 (p. 8)

Let $(A(N),\mathcal F_N,x^{0,N})$ and $(\tilde A(N),\mathcal F_N,x^{0,N})$ be two $(C,d)$-regular sequences. They share the polynomials and the initial condition, and $\mathbb E A_{ij}^2=\mathbb E\tilde A_{ij}^2$ for all $i<j$. Then for every $t$ and every family of polynomials $p_{N,i}:\mathbb R^q\to\mathbb R$ of degree at most $d$ with coefficients bounded by $B$,

$$\lim_{N\to\infty}\frac1N\sum_{i=1}^N\Big\{\mathbb E\,p_{N,i}(x^t_i)-\mathbb E\,p_{N,i}(\tilde x^t_i)\Big\}=0 .$$

Milestones

• Lemma 12 (p. 70): $x^s\le (s/e)^s e^x$ for $s,x>0$.
• (4.15) (p. 20): a sub-Gaussian variable with scale factor $C/N$ satisfies $\mathbb E|X|^s\le 2C^{s/2}(s/e)^{s/2}N^{-s/2}$.
• Proposition 1 (p. 16): $|\mathbb E(z^t_i)^m-\mathbb E(\tilde z^t_i)^m|\le KN^{-1/2}$ for $t\ge1$.
• Lemma 2, uniform bounds (pp. 22–23): $|\mathbb E z^t_i(r)^m|\le K$ and $|\mathbb E z^t_{i\to j}(r)^m|\le K$.
• Proposition 3 (p. 17), averaged over coordinates: $\frac1N\sum_i|\mathbb E(x^t_i)^m-\mathbb E(z^t_i)^m|\le KN^{-1/2}$ for $t\ge1$. The page states the bound for each $i$; that form fails when one coordinate of $x^{0,N}$ grows like $\sqrt{\log N}$, which Definition 4(3) permits, and the averaged form is what Theorem 3 needs.

In each milestone $K$ depends only on $C,d,q,t,m$, as Note 2 of the paper specifies.

Significance

Theorem 3 lets results proved for Gaussian matrices be transferred to every sub-Gaussian ensemble with the same variance profile. In the paper, it is the first link of a chain:

• Theorem 3 gives state evolution for general matrices (Theorem 4, the second mission of this series);
• state evolution, together with an analysis of AMP as a solver of $\ell_1$ minimization, gives the universality of the Donoho–Tanner phase transition for random projections of the cross-polytope (Theorem 2, the third mission).

The universality of the weak-neighborliness threshold for non-Gaussian matrices, observed numerically by Donoho and Tanner (Phil. Trans. R. Soc. A 2009), is a consequence of this chain.

The result has been proved since 2012. No machine-checked proof of it, or of any AMP state-evolution statement, is known to exist. The mission asks for a formalization of the published proof, or of any other argument. Two pieces of the proof are useful elsewhere: the absolute-moment bound for sub-Gaussian variables and the moment comparison of the message-passing iteration.

Difficulty

The first idea is a Lindeberg-type swap: replace the entries of $A$ by those of $\tilde A$ one at a time and bound each change. This does not work directly. Every iterate $x^t_i$ depends on all $N(N-1)/2$ entries through $t$ nested polynomial layers. The memory term also couples consecutive iterates through the squares $A_{ij}^2$. A single swap therefore changes every coordinate of every later iterate, and the per-swap errors have to be summed over $\Theta(N^2)$ swaps with a total error of $o(1)$.

Two features of the statement make it delicate. Only second moments of the entries are matched, so every contribution of higher moments of the entries must be shown to vanish in the limit. In addition, the AMP orbit is not itself a message-passing iteration: its moments match those of $z^t$ (Proposition 3) only because of the memory term, and without that term they do not. A formal proof also has to establish finiteness of all the moments involved, which the paper takes for granted.

Formalization scope

Vectors in $\mathbb R^q$ are Fin q → ℝ, and indices are 0-based. A polynomial is given by its coefficient vector over the exponent vectors of total degree at most $d$, as in (4.10) of the paper. This keeps random polynomials in a measurable space. The Jacobian is the explicit sum of formal partial derivatives. A sorry-free sanity file checks it against the analytic derivative on an example and checks the memory term on a small instance.

The orbit is computed by recursion on $(x^t,x^{t-1})$, with no memory term at $t=0$. The memory term uses $A_{ij}^2$ itself, not its expectation $1/N$. All random objects live on one probability space. The two sequences of Theorem 3 share one coefficient process and one initial condition.

Three readings of the printed Definition 4 are disclosed:

• sub-Gaussianity is required for all real $\lambda$ (Mathlib's HasSubgaussianMGF), not only for $\lambda > 0$;
• the scale factor is $C/N$, as the proof uses. The printed bracket $(C\lambda)^2/(2N^2)$ would rule out every ensemble with variance $1/N$ once $N > C^2$, which would make the theorem vacuous;
• the initial-condition bound holds almost surely for every $N$, not "with probability converging to one".

Every expectation appearing in a target is also asserted to be finite. Without that, a bound or a limit could hold only because Lean assigns the value $0$ to the integral of a non-integrable function. Squared Euclidean norms are written as sums of squares, never as the sup norm that Mathlib puts on Fin q → ℝ. The deterministic identities of the tree expansion (Lemma 1, Lemma 3) and the first claim of Lemma 2 are not posed, because they need the labelled-tree families of Definition 6. Contributions of that tree machinery are welcome. Moment bounds for sub-Gaussian variables and polynomial moment estimates for sums of independent variables are reusable well beyond this mission.

Selected references

• M. Bayati, M. Lelarge, A. Montanari, Universality in polytope phase transitions and message passing algorithms, Ann. Appl. Probab. 25(2):753–822, 2015. arXiv:1207.7321v2, DOI
• D. L. Donoho, A. Maleki, A. Montanari, Message-passing algorithms for compressed sensing, PNAS 106(45):18914–18919, 2009. DOI
• M. Bayati, A. Montanari, The dynamics of message passing on dense graphs, with applications to compressed sensing, IEEE Trans. Inf. Theory 57(2):764–785, 2011. DOI
• E. Bolthausen, An iterative construction of solutions of the TAP equations for the Sherrington–Kirkpatrick model, Comm. Math. Phys. 325:333–366, 2014. DOI
• D. L. Donoho, J. Tanner, Observed universality of phase transitions in high-dimensional geometry, Phil. Trans. R. Soc. A 367:4273–4293, 2009. DOI