Linear algebra

Motivation

The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.

Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.

Timeline:

• 2002, Ahlswede–Winter: matrix Laplace transform method; matrix Chernoff bound for i.i.d. summands via Golden–Thompson.
• 2010, Oliveira: a variant of the Laplace transform method used in Proposition 3.1 of the paper.
• 2010–2012, Tropp: master tail bound via Lieb's theorem (Theorem 3.6), and Theorem 5.1 / Corollary 5.2 for independent, non-identical psd summands.

Setting

All matrices are $d\times d$ complex matrices with $d\ge1$. For a self-adjoint (Hermitian) matrix $A$, $\lambda_{\max}(A)$ and $\lambda_{\min}(A)$ are its algebraically largest and smallest eigenvalues. The semidefinite order $A\preccurlyeq B$ means that $B-A$ is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if $A = Q\Lambda Q^*$ then $f(A) = Qf(\Lambda)Q^*$; this gives the matrix exponential $e^A$ and, on positive-definite matrices, the matrix logarithm $\log A$.

A random matrix is a measurable map $X:\Omega\to\mathbb C^{d\times d}$ on a probability space $(\Omega,\mathcal F,\mathbb P)$, and its expectation $\mathbb E X$ is taken entrywise. The matrix moment generating function of $X$ is $\theta\mapsto\mathbb E\,e^{\theta X}$.

The objects of the mission are independent random Hermitian matrices $X_1,\dots,X_n$ that are almost surely psd contractions: $X_k\succcurlyeq0$ and $\lambda_{\max}(X_k)\le1$. Their average expectation has extreme eigenvalues

$$\bar\mu_{\min} = \lambda_{\min}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),\qquad \bar\mu_{\max}=\lambda_{\max}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),$$

and the binary information divergence is

$$\mathrm D(a\,\|\,u) = a(\log a-\log u)+(1-a)(\log(1-a)-\log(1-u)),\qquad a,u\in[0,1].$$

In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.

Formalization targets

Goal: Theorem 5.1 (Matrix Chernoff I)

$$\mathbb P\Big\{\lambda_{\min}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\le\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\min})}\quad(0\le\alpha\le\bar\mu_{\min}),$$ $$\mathbb P\Big\{\lambda_{\max}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\ge\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\max})}\quad(\bar\mu_{\max}\le\alpha\le1).$$

Milestones

1. Theorem 3.6 (master tail bound): for every $\theta>0$ at which the mgfs exist, $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le e^{-\theta t}\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$.
2. Corollary 3.9: the same with the mgfs under one logarithm, $d\cdot\exp(-\theta t+n\log\lambda_{\max}(\frac1n\sum_k\mathbb E\,e^{\theta X_k}))$.
3. Lemma 5.8 (Chernoff mgf): $\mathbb E\,e^{\theta X}\preccurlyeq\mathbf I+(e^\theta-1)\mathbb E X$ for a random psd contraction $X$.
4. Display (5.1): $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le d\exp(-\theta t+n\log(1+(e^\theta-1)\bar\mu_{\max}))$.
5. Display (5.2): $\mathbb P\{\lambda_{\min}(\sum_kX_k)\le t\}\le d\exp(\theta t+n\log(1-(1-e^{-\theta})\bar\mu_{\min}))$.

Further statement

Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with $\lambda_{\max}(X_k)\le R$, $\mu_{\min},\mu_{\max}$ the extreme eigenvalues of $\sum_k\mathbb E X_k$,

$$\mathbb P\{\lambda_{\min}(\textstyle\sum_kX_k)\le(1-\delta)\mu_{\min}\}\le d\Big[\tfrac{e^{-\delta}}{(1-\delta)^{1-\delta}}\Big]^{\mu_{\min}/R},\quad \mathbb P\{\lambda_{\max}(\textstyle\sum_kX_k)\ge(1+\delta)\mu_{\max}\}\le d\Big[\tfrac{e^{\delta}}{(1+\delta)^{1+\delta}}\Big]^{\mu_{\max}/R}.$$

Significance

Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor $d$, which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound $\mathbb E\lambda_{\max}(\sum_kX_k)\le C\max\{\mu_{\max},R\log d\}$.

The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.

Difficulty

The scalar Chernoff argument uses $\mathbb E\,e^{\theta(X+Y)}=\mathbb E\,e^{\theta X}\,\mathbb E\,e^{\theta Y}$ for independent $X,Y$. For matrices $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. $\lambda_{\max}$, $\lambda_{\min}$ are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "$\lambda_{\max}\le1$" hold almost surely. The sequence has $n\ge1$ terms wherever an average $1/n$ appears. An infimum over $\theta>0$ is stated as a bound for every admissible $\theta>0$; integrability of $e^{\theta X_k}$ is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean $\log 0=0$, so at the boundary values $\bar\mu\in\{0,1\}$ the divergence is finite where the paper's is $+\infty$; this only weakens the stated bound.

A formalization in which $d=0$ (empty spectrum, $\lambda_{\max}=0$) or $n=0$ (the average $1/0=0$) were allowed, or in which the range of $\alpha$ were dropped, would state a different, partly false theorem; these cases are excluded.

A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in $\theta$. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede, A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• 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
• 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

Motivation

A spectral sparsifier of a weighted graph $G$ is a graph $\widetilde G$ on the same vertices, with few edges, whose Laplacian quadratic form is within a factor $\sigma$ of that of $G$ on every vector. Spielman and Teng introduced the notion in their work on nearly-linear-time solvers for symmetric diagonally dominant linear systems (Spielman–Teng 2004; arXiv:0808.4134): a sparsifier can replace a dense graph as a preconditioner, and it preserves every cut value up to the same factor, strengthening the cut sparsifiers of Benczúr and Karger (BK96).

Their construction first handles graphs whose edge weights lie in a bounded range. Arbitrary weights need an extra idea, which §10.2 of Spectral Sparsification of Graphs formalizes as Lemma 10.2 (Pullback): when a graph's vertex classes are held together by edges far heavier than those between them, one may contract each class to a single vertex, sparsify the much smaller contracted graph, and pull the result back to the original vertices. The approximation factor degrades only by $(1+1/c)^2$, where $c$ measures the gap between heavy and light weights. The same contraction idea goes back to Benczúr and Karger's treatment of weighted cut sparsifiers.

Setting

A weighted graph $G=(V,E,w)$ on a finite set $V$, $n=|V|$, is a symmetric function $w:V\times V\to\mathbb R_{\ge 0}$ with $w(v,v)=0$; its edges are the pairs with $w(u,v)\ne 0$. Its Laplacian quadratic form is

$$x^TL_Gx=\sum_{(u,v)\in E}w(u,v)\,(x(u)-x(v))^2,\qquad x\in\mathbb R^V .$$

A graph $\widetilde G$ is a $\sigma$-approximation of $G$ if $\frac1\sigma x^TL_{\widetilde G}x\le x^TL_Gx\le\sigma\, x^TL_{\widetilde G}x$ for all $x$. We write $G\preccurlyeq G'$ when $x^TL_Gx\le x^TL_{G'}x$ for all $x$, $G+G'$ for the graph whose weights are the sums, and $(u,v)$ for the single edge $\{u,v\}$ of weight $1$.

Let $V_1,\dots,V_k$ be a partition of $V$ with map $\pi:V\to\{1,\dots,k\}$. Write $E_0=\partial(V_1,\dots,V_k)$ for the edges between different parts, $E_1=E-E_0$, and $G_0=(V,E_0,w)$, $G_1=(V,E_1,w)$. The contraction of $G$ under $\pi$ is the graph $H$ on $\{1,\dots,k\}$ with weight $z(i,j)=\sum_{\pi(u)=i,\,\pi(v)=j}w(u,v)$ for $i\ne j$ and no self-loops. Given a graph $\widetilde H$ on $\{1,\dots,k\}$, a graph $\widetilde G$ on $V$ is a pullback of $\widetilde H$ under $\pi$ if every edge of $\widetilde G$ joins different parts, $\widetilde H$ is the contraction of $\widetilde G$, and for every edge $(i,j)$ of $\widetilde H$ exactly one edge $(u,v)$ of $\widetilde G$ has $\pi(u)=i$, $\pi(v)=j$. A pullback thus has as many edges as $\widetilde H$.

Formalization targets

Goal: Lemma 10.2 (Pullback), pp. 36–37

Let $0\le\epsilon<1/2$, $c\ge3$, let $\widetilde H$ be a $(1+\epsilon)$-approximation of the contraction of $G_0$ under $\pi$, and let $\widetilde G_0$ be a pullback of $\widetilde H$. Assume (1) each $V_i$ is connected by edges in $E_1$, (2) every edge in $E_1$ has weight at least $c^2n^3$, (3) every edge in $E_0$ has weight $1$. Then

$$\widetilde G_0+G_1\ \text{ is an }\ \alpha\text{-approximation of } G,\qquad \alpha=(1+\epsilon)\Big(1+\frac1c\Big)^2 .$$

Milestones (proof of Lemma 10.2, pp. 37–38)

Choose representatives $v_i\in V_i$; let $F$, $\widetilde F$ be the copies of $H$, $\widetilde H$ on $\{v_1,\dots,v_k\}$, and $I=F+G_1$, $\widetilde I=\widetilde F+G_1$.

• Lemma 10.3 (path inequality): for a path from $u$ to $v$ with edge weights $w_1,\dots,w_k>0$, $(u,v)\preccurlyeq(1/w_1+\dots+1/w_k)F$.
• (20), (21): for $a,b$ in different parts and $f$ the unit edge between $v_{\pi(a)},v_{\pi(b)}$,

$$(a,b)\preccurlyeq\Big(1+\frac1c\Big)\Big(f+\frac{1}{cn^2}G_1\Big),\qquad f\preccurlyeq\Big(1+\frac1c\Big)\Big((a,b)+\frac{1}{cn^2}G_1\Big).$$

• Summed bound: $G_0\preccurlyeq(1+1/c)\,[F+\tfrac1{2c}G_1]$.
• Claim (a): $I$ is a $(1+1/c)$-approximation of $G$.
• Claim (b): $\widetilde I$ is a $(1+\epsilon)$-approximation of $I$.
• Claim (c): $\widetilde I$ is a $(1+1/c)$-approximation of $\widetilde G_0+G_1$.

The constants are the paper's; the goal is the lemma as printed.

Significance

Lemma 10.2 is the reduction from arbitrary weights to bounded weights in Spielman and Teng's sparsification algorithm (Sparsify, §10.2): the edges of each weight scale are sparsified on a graph in which all much heavier edges have been contracted, so the number of vertices handled at each scale stays small, and the total size of the sparsifier is only a logarithmic factor larger than in the bounded-weight case. The statement itself is purely about quadratic forms and holds for any approximation $\widetilde H$ of the contraction, however it was obtained; it applies equally to later sparsification methods such as sampling by effective resistances.

The lemma is proved in the paper. As far as is known, none of these statements has a machine-checked proof: Mathlib has the Laplacian of a simple graph (SimpleGraph.lapMatrix) but no weighted Laplacian order, no contraction of weighted graphs and no notion of spectral approximation. The mission produces those objects and a complete formal proof of the lemma and its intermediate claims.

Difficulty

The individual steps are elementary, but the proof combines three kinds of bookkeeping. Lemma 10.3 is a Cauchy–Schwarz inequality along a path, which must be applied to a path assembled from two walks inside parts and one edge between representatives; obtaining a simple path of length at most $n$ from the connectivity hypothesis requires shortening walks. The summed bounds require recognising that the copies of the unit edges between representatives add up exactly to $F$, which uses hypothesis 3 and the fact that contraction counts each edge between two parts once. Claim (c) needs, in addition, that the total weight of $\widetilde F$ is at most $(1+\epsilon)$ times that of $F$ and that each pullback edge has the weight of its image edge. The constants are tight in one place: $(1+1/c)(1+\epsilon)\le 2$ requires both $c\ge3$ and $\epsilon\le 1/2$.

A natural shortcut, comparing $\widetilde G_0$ with $G_0$ directly, fails: $\widetilde G_0$ and $G_0$ have different edges, and their Laplacians are only comparable through the heavy intra-part edges.

Formalization scope

A weighted graph is a function w : V → V → ℝ on a Fintype V with IsWGraph w (symmetric, nonnegative, zero diagonal); sums and scalar multiples are pointwise. lapForm w x is $\frac12\sum_{u,v}w(u,v)(x(u)-x(v))^2$, IsApprox σ w̃ w keeps both inequalities of the definition, and GraphLE is $\preccurlyeq$. The partition is a surjective map π : V → Fin k (nonempty parts). $G_0$, $G_1$ are crossPart w π, intraPart w π; hypothesis 1 is reachability, between any two vertices of the same part, in the simple graph of $E_1$-edges. Representatives are any r : Fin k → V with π (r i) = i, and liftAlong r z places a graph on Fin k on them; the goal does not mention representatives. $n$ is Fintype.card V.

Two hypotheses implicit in the paper are explicit: $\epsilon\ge0$ (with $\epsilon<0$ the lemma is false), and that every edge of a pullback joins two different parts (contraction cannot see an edge inside a part, so without this a pullback could carry an arbitrary heavy edge and the lemma would be false). In Lemma 10.3 the edge weights are positive and the path has at least one edge.

A trivializing formalization is ruled out: dropping hypothesis 2 or 3, allowing $\epsilon<0$ or intra-part pullback edges, or letting the pullback forget the uniqueness of the edge over each $(i,j)$ makes the statement false or weaker, and stating only one of the two inequalities of $\sigma$-approximation is a different theorem. Every statement here keeps both.

The algorithm Sparsify and its analysis (Lemma 10.4, Theorem 10.5, Proposition 10.6, Theorem 10.7, Lemmas 10.8–10.9) and all running-time claims are out of scope. The weighted Laplacian form, its additivity and nonnegativity, and the transport of a quadratic form along an injective vertex map are reusable beyond this mission; contributions of such general lemmas, and a proof of Lemma 10.3 by Cauchy–Schwarz, are welcome.

Selected references

• D. A. Spielman, S.-H. Teng, Spectral Sparsification of Graphs, arXiv:0808.4134v3, 2010; SIAM J. Comput. 40(4), 2011. https://arxiv.org/abs/0808.4134
• D. A. Spielman, S.-H. Teng, Nearly-Linear Time Algorithms for Graph Partitioning, Graph Sparsification, and Solving Linear Systems, STOC 2004. https://arxiv.org/abs/cs/0310051
• A. A. Benczúr, D. R. Karger, Approximating s-t Minimum Cuts in Õ(n²) Time, STOC 1996; Randomized Approximation Schemes for Cuts and Flows in Capacitated Graphs, arXiv:cs/0207078. https://arxiv.org/abs/cs/0207078
• P. Diaconis, D. Stroock, Geometric Bounds for Eigenvalues of Markov Chains, Ann. Appl. Probab. 1(1), 1991. https://doi.org/10.1214/aoap/1177005980

Motivation

Minimizing the sum of the $k$ largest eigenvalues of a symmetric matrix that depends affinely on parameters is a basic problem of eigenvalue optimization (survey: A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 1996, doi:10.1017/S0962492900002646). Its objective is convex, and $f_k$ is differentiable at $B$ exactly when $\lambda_k(B)>\lambda_{k+1}(B)$; at optimal solutions the eigenvalues tend to coalesce, which makes the problem a model problem of nonsmooth optimization. G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues (Math. Oper. Res. 23(2), 1998, doi:10.1287/moor.23.2.339), gives a quantitative explanation in terms of the number of free parameters.

The paper also proves a bound on the rank of extreme points of semidefinite programs, now often called the Pataki bound (also obtained by Barvinok, 1995): an extreme point $X$ of $\{X\succeq0: A_i\bullet X=b_i,\ i\le m\}$ satisfies $\operatorname{rank}X(\operatorname{rank}X+1)/2\le m$. This bound is used throughout low-rank semidefinite optimization, for instance in the Burer–Monteiro approach.

Setting

$\mathcal S^n$ is the space of real symmetric $n\times n$ matrices, $X\succeq0$ means $X$ is symmetric positive semidefinite, and $A\bullet B=\sum_{i,j}a_{ij}b_{ij}$. For $B\in\mathcal S^n$, $\lambda_1(B)\ge\dots\ge\lambda_n(B)$ are its eigenvalues and, for $k\in\{1,\dots,n\}$,

$$f_k(B)=\lambda_1(B)+\dots+\lambda_k(B).$$

The multiplicity $\operatorname{mult}(\lambda_i(B))$ is the largest $p\ge1$ with $\lambda_j(B)=\dots=\lambda_{j+p-1}(B)$ for some $j\le i\le j+p-1$.

A face of a convex set $S$ is a convex $F\subseteq S$ such that $x\in F$, $y,z\in S$, $x=\tfrac12(y+z)$ imply $y,z\in F$; an extreme point is a one-point face; $\dim S$ is the maximal number of affinely independent points of $S$, minus one. Write $t(i)=i(i+1)/2$ and

$$\tau(l,r,s)=\max\{\,i+j:\ t(i)+t(j)\le l,\ i\le r,\ j\le s\,\}.$$

Let $A_0,A_1,\dots,A_m\in\mathcal S^n$ be linearly independent, $A(x)=A_0+\sum_{i=1}^mx_iA_i$, and assume $m\ge1$ and $k<n$ (the standing assumptions of §4). The affine eigenvalue problem is

$$(EV_k)\qquad\min\{f_k(A(x)):\ x\in\mathbb R^m\},$$

and $\Theta$ denotes its set of optimal solutions, a closed convex set. For $B\in\mathcal S^n$ the semidefinite program

$$\min\ kz+I\bullet V\quad\text{s.t.}\quad V,W\succeq0,\quad zI+V-W=B \tag{3.14}$$

has optimal value $f_k(B)$; $\Omega_k(B)$ is its set of optimal solutions $(z,V,W)$.

Formalization targets

Goal: Theorem 4.3

If $x^*$ is an extreme point of $\Theta$ and $m>k(n-k)$, then

$$\lambda_k(A(x^*))=\lambda_{k+1}(A(x^*))\qquad\text{and}\qquad \operatorname{mult}(\lambda_k(A(x^*)))\ \ge\ n-\tau\big(t(n)-m-1,\,k-1,\,n-k-1\big).$$

Milestones

1. Theorem 2.1: on a face $F$ of the primal feasible set, $t(\operatorname{rank}X)\le m+\dim F$; on a face $G$ of the dual feasible set, $t(\operatorname{rank}Z)\le t(n)-m+\dim G$.
2. Theorem 2.2: the multi-block version $\sum_jt(\operatorname{rank}X_j)\le m-q+\dim G$ for programs with $p$ semidefinite blocks and $q$ free variables.
3. Lemmas 3.1, 3.2 and Theorem 3.3: the optimal value of (3.14) and an explicit description of $\Omega_k(B)$ through an eigendecomposition $B=Q\operatorname{Diag}(\lambda)Q^T$.
4. The rank identity of §3: $\operatorname{rank}V+\operatorname{rank}W+\operatorname{mult}(\lambda_k(B))=n$ on $\Omega_k(B)$ when $\lambda_k(B)=\lambda_{k+1}(B)$.
5. Lemma 4.2 and (4.31): $\{x^*\}\times\Omega_k(A(x^*))$ is a face of the feasible set of the lifted SDP (4.26), of dimension $1$ or $0$ according as $\lambda_k>\lambda_{k+1}$ or $\lambda_k=\lambda_{k+1}$.
6. Lemma 4.1: $\Theta$ contains no line, so it has extreme points whenever it is nonempty.

Significance

The theorem says that once the number of free parameters $m$ exceeds $k(n-k)$, the $k$-th and $(k+1)$-st eigenvalues necessarily coincide at extreme optimal solutions, so $f_k\circ A$ is typically nonsmooth at its minimizers, and it bounds from below the dimension of the subdifferential $\partial f_k(A(x^*))$, which is $t(\operatorname{mult}(\lambda_k))$. The intermediate rank bounds of §2 are reusable on their own for any semidefinite program.

The results are proved in the paper. As far as is known, none of them (neither the Pataki rank bound, nor the semidefinite characterization of $f_k$, nor Theorem 4.3) has a machine-checked proof. Formalizing them produces a library of faces and dimensions of spectrahedra, the SDP representation of the Ky Fan sum $f_k$, and the multiplicity bound itself.

Difficulty

Extremality of $x^*$ in $\Theta$ is a statement in the parameter space $\mathbb R^m$ and gives no direct information on the spectrum of $A(x^*)$: perturbation arguments on the eigenvalues alone break down precisely at the coalesced eigenvalues the theorem is about, where $f_k$ is not differentiable. The quantitative bound (4.30) also needs more than the optimal value $f_k(A(x^*))$: it depends on the whole optimal set $\Omega_k(A(x^*))$, on the dimension of faces of spectrahedra, and on an exact count relating the ranks of the optimal $V,W$ to the multiplicity of $\lambda_k$. None of these (faces and dimension of spectrahedra, the semidefinite representation of $f_k$, eigenvalue run lengths) is in Mathlib.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $A\bullet B$ is the published BurerMonteiro.RankIncrease.frob, the primal and dual feasible sets are the published IsPrimalFeasible/IsDualFeasible, and $\lambda_i(B)$ is the published ProjLikeRetr.Spectral.eig B ⟨i-1,_⟩ (Mathlib's nonincreasing eigenvalues, 0-based). Every matrix whose eigenvalues are taken is assumed symmetric. Faces, extreme points and dimension are defined as on p. 341; dimension is integer valued with $\dim\emptyset=-1$. All rank bounds are compared in $\mathbb Z$. $\Theta$ is the argmin set $\{x: f_k(A(x))\le f_k(A(y))\ \forall y\}$ and $\Omega_k(B)$ is the set of feasible points no worse than every feasible point; no infimum is used. Optimal values are stated as least elements of the set of feasible objective values.

Hypotheses added relative to the page, each disclosed in its item: $1\le k<n$ in the statements of §3, which mention $\lambda_{k+1}$; $k\ge1$ (p. 340) in every §4 statement; one common matrix order in Theorem 2.2; and $\lambda_k(B)=\lambda_{k+1}(B)$ in the rank identity of p. 348, which is false as printed when $\lambda_k(B)>\lambda_{k+1}(B)$ ($n=2$, $k=1$, $B=\operatorname{diag}(2,0)$ gives $3\ne2$) and is used in the paper only in the equal case. The linear independence of $A_0,\dots,A_m$ is kept with $A_0$ included, as on p. 348.

Trivializing formalizations are ruled out: $\Theta$ is not defined through a possibly junk infimum, a face must be convex and contained in the set, the dimension is not a junk $0$, $\operatorname{mult}$ is the run length of equal eigenvalues and not a constant or an index, and the eigenvalues are only ever taken of symmetric matrices.

A complete development needs: the rank–dimension bound for faces of spectrahedra (reusable for any SDP), the semidefinite characterization of $f_k$ with its optimal set, and convexity facts on $\Theta$. Proofs of any milestone, alternative proofs of the rank bounds, and the general smooth case of §5 are welcome.

Selected references

• G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23(2), 339–358, 1998. https://doi.org/10.1287/moor.23.2.339
• A. I. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13, 189–202, 1995. https://doi.org/10.1007/BF02574037
• M. L. Overton and R. S. Womersley, Optimality conditions and duality theory for minimizing sums of the largest eigenvalues of symmetric matrices, Mathematical Programming 62, 321–357, 1993. https://doi.org/10.1007/BF01585173
• F. Alizadeh, Interior point methods in semidefinite programming with applications to combinatorial optimization, SIAM Journal on Optimization 5(1), 13–51, 1995. https://doi.org/10.1137/0805002
• A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 149–190, 1996. https://doi.org/10.1017/S0962492900002646
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

Motivation

Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.

Setting

For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.

Formalization target

Prove the strict bound

$$\alpha_{\mathbb C}>\frac{93}{200}=0.465.$$

The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.

The selected formal target is OAI.MatrixMultiplication.complex_alpha_gt_93_div_200.

Significance and status

Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.

Formalization scope

Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.

Selected references

• OpenAI, Complex Matrix Multiplication Below 2.258 and Rectangular Bounds, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

The discrete Fourier transform of length $n$ is computed by the fast Fourier transform with $O(n\log n)$ arithmetic operations, and this has been the benchmark since Cooley and Tukey (1965). Whether $\Omega(n\log n)$ operations are necessary is one of the basic open questions of algebraic complexity theory. Lower bounds of order $n\log n$ are known only under restrictions on the algorithm: bounded coefficients, unitary $2\times2$ gates on exactly $n$ registers, or bounded conditioning of intermediate maps. In the unrestricted model of linear circuits, where coefficients are arbitrary complex numbers and only arithmetic operations are counted, the question remained open. This mission concerns that unrestricted question.

Timeline

• 1958. Good gives the multidimensional (coprime-factor) form of the Fourier transform (doi:10.1111/j.2517-6161.1958.tb00300.x).
• 1965. Cooley and Tukey publish the fast Fourier transform (doi:10.1090/S0025-5718-1965-0178586-1).
• 1969–1970. Rabiner, Schafer and Rader (chirp $z$-transform) and Bluestein reduce arbitrary lengths to convolution (doi:10.1109/TAU.1969.1162034, doi:10.1109/TAU.1970.1162132).
• 1973. Morgenstern proves an $\Omega(n\log n)$ lower bound for linear circuits with bounded coefficients (doi:10.1145/321752.321761).
• 2013–2014. Ailon proves lower bounds for $2\times2$ unitary gate models and for well-conditioned computations (arXiv:1305.4745, arXiv:1403.1307).
• 2023. Alman and Rao improve the leading constants for power-of-two transforms via matrix non-rigidity (doi:10.1145/3564246.3585188).
• 2025. Alman and Li characterize asymptotic sizes of depth-two circuits for Kronecker powers (arXiv:2509.14489).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims that the $\Omega(n\log n)$ lower bound fails in the unrestricted complex linear-circuit model.

Setting

For $n\ge2$ let $\zeta_n=e^{2\pi i/n}$ and $F_n=(\zeta_n^{jk})_{0\le j,k<n}$. A linear circuit of length $n$ has inputs $x_0,\dots,x_{n-1}$ and the constant $0$, followed by a finite sequence of gates. Each gate computes $u+v$, $u-v$ or $\lambda u$ from previously available values $u,v$, where $\lambda\in\mathbb C$ is a fixed coefficient; each gate costs one. Values may be reused arbitrarily, and the $n$ outputs are designated available values. The circuit computes $F_n$ if its outputs equal $F_nx$ for every $x\in\mathbb C^n$. Coefficients may depend on $n$ and have no bound on size or description; depth, storage and conditioning are unrestricted. Let $L(n)$ be the minimum number of gates.

Formalization targets

Goal: Theorem 1.1

$$\liminf_{n\to\infty}\frac{L(n)}{n\log_2 n}=0,$$

equivalently: for every $c>0$ and every $N_0\ge2$ there are $n\ge N_0$ and an exact circuit for $F_n$ with fewer than $c\,n\log_2 n$ gates. The Lean statement OAI.ExactFourier.main_theorem is this second form and is open on the platform.

The statement does not assert an upper bound for every length, a uniform construction, or anything about numerical stability. A companion OpenAI preprint gives a quantitative all-length bound in a model that also charges coefficient preparation; that result is not part of this mission.

Significance

The theorem refutes the assertion that $L(n)\ge c\,n\log_2n$ for some fixed $c>0$ and all large $n$ in the unrestricted linear model. It shows that the known lower bounds necessarily depend on their restrictions (bounded coefficients, conditioning, unitary gates). The mechanism, a single finite tensor saving amplified through tensor powers, is a general tool: one strict improvement over the standard axis-by-axis algorithm for one tensor power of one nonmonomial matrix yields an exponent improvement for all tensor powers.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The existence part of the argument is non-constructive (it proceeds by contradiction through price functions and compactness), so a formal proof is a meaningful check.

Difficulty

Leading-constant improvements of the FFT do not change the $n\log n$ scale, and every classical structural algorithm (Cooley–Tukey, Good–Thomas, chirp) has that scale. A gain in the exponent of the logarithm needs a saving that compounds across many tensor factors; but a saving for one tensor power of a small matrix does not obviously transfer to Fourier matrices of growing length, because Fourier factorizations introduce diagonal twiddle factors and change the coordinate set. In addition, the existence of a single finite saving is itself not exhibited explicitly and must be proved.

Formalization scope

• Gate w is add i j, sub i j or scale c i with c : ℂ, referencing the $w$ values available so far.
• Program n k is a list of $k$ gates in topological order; values $0,\dots,n-1$ are the inputs and value $n$ is the constant $0$ (via Fin.snoc x 0).
• Circuit n has size, a program of that size, and outputs : Fin n → Fin (n+1+size); output selection is free.
• fourierMatrix n j k = zeta n ^ (j*k) with zeta n = exp(2πi/n); Computes is equality with mulVec for every input.
• MainStatement: for every real $c>0$ and $N_0\ge2$ there are $n\ge N_0$ and a computing circuit with size < c * n * logb 2 n.

A complete development needs tensor products of matrices and circuits, the Chinese Remainder (Good–Thomas) identification of $F_{rs}$ with $F_r\otimes F_s$ for coprime $r,s$, a Toeplitz/Vandermonde factorization of $F_r$ on its own coordinates, and the price-function existence argument (separation, compactness, feedback). Contributions formalizing Lemma 2.3 (tensor amplification) and Proposition 3.4 (transfer of a finite win to Fourier circuits) are natural first steps.

Selected references

• OpenAI, Finite tensor savings and exact Fourier circuits, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026/main.pdf
• J. W. Cooley, J. W. Tukey, An algorithm for the machine calculation of complex Fourier series, Math. Comp., 1965. https://doi.org/10.1090/S0025-5718-1965-0178586-1
• J. Morgenstern, Note on a lower bound on the linear complexity of the fast Fourier transform, J. ACM, 1973. https://doi.org/10.1145/321752.321761
• N. Ailon, A lower bound for Fourier transform computation in a linear model over 2×2 unitary gates, preprint, 2013. https://arxiv.org/abs/1305.4745
• N. Ailon, An $\Omega((n\log n)/R)$ lower bound for Fourier transform computation in the $R$-well conditioned model, preprint, 2014. https://arxiv.org/abs/1403.1307
• J. Alman, K. Rao, Faster Walsh–Hadamard and discrete Fourier transforms from matrix non-rigidity, STOC 2023. https://doi.org/10.1145/3564246.3585188
• I. J. Good, The interaction algorithm and practical Fourier analysis, J. R. Stat. Soc. B, 1958. https://doi.org/10.1111/j.2517-6161.1958.tb00300.x
• J. Alman, B. Li, Kronecker powers, orthogonal vectors, and the asymptotic spectrum, preprint, 2025. https://arxiv.org/abs/2509.14489

Motivation: the matrix-multiplication exponent

Multiplying two $n\times n$ matrices by the schoolbook method costs about $n^3$ operations. The matrix-multiplication exponent $\omega_F$ of a field $F$ is the infimum of exponents $\tau$ such that $n\times n$ matrices over $F$ can be multiplied with $O(n^{\tau+o(1)})$ additions, subtractions and multiplications. It governs the asymptotic cost of a central bilinear operation and of the many algorithms built from it (determinants, inversion, linear systems). Bounding $\omega$ has driven algebraic complexity theory since 1969. In recent years the bounds have moved in the third and fourth decimal place, with each improvement coming from a finer analysis of the same tensor-power framework.

Background

• 1969 — Strassen's seven-product algorithm gives $\omega\le\log_27$ (Strassen 1969).
• 1980–1987 — Approximate bilinear algorithms (Bini 1980), the asymptotic sum inequality (Schönhage 1981) and the laser method (Strassen 1987).
• 1990 — Coppersmith and Winograd introduce the tensor family $\mathrm{CW}_q$ and progression-free extraction (J. Symbolic Comput. 1990).
• 2010–2014 — Higher tensor powers: Stothers (fourth power; with Davie, Proc. Roy. Soc. Edinburgh 2013), Vassilevska Williams (eighth power, STOC 2012), Le Gall (thirty-second power, ISSAC 2014).
• 2023–2024 — The refined laser method gives $\omega<2.3728596$ (Alman–Vassilevska Williams, TheoretiCS 2024). Asymmetric hashing reduces combination loss (Duan–Wu–Zhou). Finer variable sharing follows (Vassilevska Williams–Xu–Xu–Zhou).
• 2024–2026 — Successive asymmetric compatibility tests (Alman–Duan–Vassilevska Williams–Xu–Xu–Zhou, arXiv:2404.16349). Dupont et al. optimize the eighth-power instance of this framework to $\omega<2.371177$ (arXiv:2608.16884).
• 2026 — An OpenAI preprint, Staggered extraction for exact matrix multiplication over every field (OpenAI Math Release, September 24, 2026), claims $\omega_F<2.371054886006746$ for every fixed field $F$, including every positive characteristic. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Fix a field $F$. An arithmetic program is a straight-line sequence of gates, each a constant from $F$, an input entry, or the sum, difference or product of two earlier gates. Its cost counts the addition, subtraction and multiplication gates. A program multiplies $n\times n$ matrices if designated registers equal the entries of $AB$ for every pair of input matrices $A,B$ over $F$. A real number $\tau$ is admissible if for every $\varepsilon>0$ there is $C>0$ such that for every $n\ge1$ some correct program has cost at most $C\,n^{\tau+\varepsilon}$, and

$$\omega_F=\inf\{\tau\in\mathbb R:\ \tau\text{ admissible over }F\}.$$

In Lean this is MatrixAllFields.MatrixMultiplication.Arithmetic.omega F, defined for every F : Type u with [Field F].

Formalization targets

Goal: the exponent bound over every field (Theorem 1.1)

$$\forall\,F\ \text{field}:\qquad \omega_F<2.371054886006746 .$$

The Lean statement also contains the numerical comparison $2.371054886006746<2.371056$, which carries no mathematical content (the source writes the comparison as $<2.371054887$). This is Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's argument and certificate are correct, the theorem lowers the best stated bound on $\omega$ from $2.371177$ (Dupont et al.) to $2.371055$, and it does so uniformly over all fields, with exact algorithms in every positive characteristic. Any improvement in $\omega$ lowers the exponent of every algorithm reducible to matrix multiplication. The method — pooling directional capacities across extraction depths and staggering lots so that one lot sits at each splitting stage — shows that combination losses in the asymmetric framework can be traded across depths.

Formalizing it. Bounds of this type rest on long chains of tensor-power constructions, recovery arguments and large rational parameter tables, checked in the source by an accompanying verifier with interval certificates for logarithms. A machine-checked proof would certify the whole chain from the arithmetic model to the final rational inequality. It would also give Mathlib the asymptotic sum inequality and Coppersmith–Winograd machinery, which every future bound on $\omega$ needs.

Difficulty

Every recent improvement fights extraction losses. Restricting a tensor power to a direct sum of independent matrix products wastes variables whenever whole blocks must be disjoint, while the final products only need disjoint subsets. Prescribed marginals may also allow several joint distributions. Earlier analyses take the minimum of three directional capacities separately at each depth, so a shortage on one side at one depth is lost. Using capacity across depths requires that variables deleted in earlier extractions (to resolve conflicts or impose type conditions) can still be recovered exactly, over the original field and with only subexponentially many extra copies. Positive characteristic rules out arguments that divide by small integers or rely on characteristic-zero identities.

Formalization scope

• The model is division-free straight-line programs over an arbitrary field F : Type u, with free constants from $F$ and unit cost for add, sub and mul. This matches the source's "scalar additions and multiplications".
• AdmissibleExponent F τ asks, for each $\varepsilon>0$, for one constant $C>0$ that works for every $n\ge1$. omega F is the sInf of the admissible set, which is nonempty (schoolbook algorithm) and bounded below by the output size, so a junk value cannot make the strict inequality true.
• The goal quantifies over every field, including finite fields, so a proof cannot use characteristic-zero arguments or embeddings into $\mathbb C$.
• The second conjunct is a trivially true rational comparison and can be ignored.
• Infrastructure needed: tensor rank and border rank over arbitrary fields, the asymptotic sum inequality, the Coppersmith–Winograd tensor and its powers, method-of-types counting, and verified rational/logarithm interval arithmetic for the parameter certificate. All of this is reusable for other matrix-multiplication results.

Selected references

• V. Strassen, Gaussian elimination is not optimal, Numer. Math. 13 (1969), 354–356. https://doi.org/10.1007/BF02165411
• D. Bini, Relations between exact and approximate bilinear algorithms. Applications, Calcolo 17 (1980), 87–97. https://doi.org/10.1007/BF02575865
• A. Schönhage, Partial and total matrix multiplication, SIAM J. Comput. 10 (1981), 434–455. https://doi.org/10.1137/0210032
• V. Strassen, Relative bilinear complexity and matrix multiplication, J. reine angew. Math. 375/376 (1987), 406–443. https://doi.org/10.1515/crll.1987.375-376.406
• D. Coppersmith and S. Winograd, Matrix multiplication via arithmetic progressions, J. Symbolic Comput. 9 (1990), 251–280. https://doi.org/10.1016/S0747-7171(08)80013-2
• A. M. Davie and A. J. Stothers, Improved bound for complexity of matrix multiplication, Proc. Roy. Soc. Edinburgh Sect. A 143 (2013), 351–369. https://doi.org/10.1017/S0308210511001648
• V. Vassilevska Williams, Multiplying matrices faster than Coppersmith–Winograd, STOC 2012, 887–898. https://doi.org/10.1145/2213977.2214056
• F. Le Gall, Powers of tensors and fast matrix multiplication, ISSAC 2014, 296–303. https://arxiv.org/abs/1401.7714v1
• J. Alman and V. Vassilevska Williams, A refined laser method and faster matrix multiplication, TheoretiCS 3 (2024), Art. 21. https://doi.org/10.46298/theoretics.24.21
• R. Duan, H. Wu and R. Zhou, Faster matrix multiplication via asymmetric hashing, arXiv:2210.10173. https://arxiv.org/abs/2210.10173v5
• V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, New bounds for matrix multiplication: from alpha to omega, arXiv:2307.07970. https://arxiv.org/abs/2307.07970v2
• J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, More asymmetry yields faster matrix multiplication, arXiv:2404.16349v3. https://arxiv.org/abs/2404.16349v3
• E. Dupont et al., Improving the matrix multiplication exponent with modern optimization, arXiv:2608.16884 (2026). https://doi.org/10.48550/arXiv.2608.16884
• OpenAI, Staggered extraction for exact matrix multiplication over every field, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026.pdf

Motivation

Many data problems ask for a matrix of low rank from far fewer linear measurements than it has entries: matrix completion (recommender systems, where a few ratings of a large user–item table are observed), system identification, and quantum state tomography. Minimizing the rank under the measurement constraints is NP-hard in general. The standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values, and recovers the low-rank matrix exactly when the measurement map is well conditioned on low-rank matrices (Recht, Fazel, Parrilo 2010; Candès, Recht 2009).

Solving the nuclear norm problem at scale is itself a numerical challenge: interior point methods do not scale, and first-order methods such as singular value thresholding (Cai, Candès, Shen 2010) need many iterations. Fornasier, Rauhut and Ward proposed an alternative, iteratively reweighted least squares for matrices (IRLS-M), which replaces the nonsmooth problem by a sequence of weighted least squares problems whose weights are recomputed from the current iterate. It is the matrix analogue of the IRLS method for sparse vectors of Daubechies, DeVore, Fornasier, Güntürk 2010, and a closely related algorithm was studied at the same time by Mohan and Fazel (Allerton 2010; journal version JMLR 2012).

Timeline. 2008–2010: nuclear norm recovery under rank restricted isometry (Recht–Fazel–Parrilo) and the rank null space property (Recht–Xu–Hassibi). 2010: convergence of IRLS for $\ell_1$ under the vector null space property (Daubechies et al.). 2010–2011: IRLS-M and its convergence under the strong rank null space property (this paper, arXiv:1010.2471, SIAM J. Optim. 21(4), 2011).

Setting

Throughout, $X$ is a real $n\times p$ matrix with $n\le p$, with singular values $\sigma_1(X)\ge\dots\ge\sigma_n(X)\ge0$. The Frobenius norm is $\|X\|_F$, the nuclear norm is $\|X\|_*=\sum_i\sigma_i(X)$, and $\langle X,Y\rangle=\sum_{i,j}X_{ij}Y_{ij}$. A linear measurement map $\mathcal S:\mathbb R^{n\times p}\to\mathbb R^m$ is given by matrices $A_1,\dots,A_m$ through $\mathcal S(X)_l=\langle A_l,X\rangle$; the data are $\mathscr M\in\mathbb R^m$.

The best $k$-rank approximation error is $\rho_k(X)_*=\min_{\operatorname{rank}Z\le k}\|X-Z\|_*$. The map $\mathcal S$ has the strong rank null space property (SRNSP) of order $k$ with constant $\eta\in(0,1)$ if every nonzero $X\in\ker\mathcal S$ and every split $X=X_1+X_2$ with $\operatorname{rank}X_1\le k$ admit another split $X=H_1+H_2$ with $\operatorname{rank}H_1\le2k$, $\langle H_1,H_2\rangle=0$, $X_1H_2^{\mathsf T}=0$, $X_1^{\mathsf T}H_2=0$ and $\|H_1\|_*\le\eta\|H_2\|_*$.

For $\varepsilon>0$ the weight of $X$ is $W=U\Sigma_\varepsilon^{-1}U^{\mathsf T}$, where $XX^{\mathsf T}=U\Sigma^2U^{\mathsf T}$ and $\Sigma_\varepsilon=\operatorname{diag}(\max\{\sigma_j,\varepsilon\})$. The IRLS-M algorithm with parameters $K\in\mathbb N$ and $\gamma>0$ starts from $W^0=I$, $\varepsilon_0=1$ and repeats

$$X^\ell\in\arg\min_{\mathcal S(X)=\mathscr M}\|(W^{\ell-1})^{1/2}X\|_F^2,\qquad\varepsilon_\ell=\min\{\varepsilon_{\ell-1},\gamma\sigma_{K+1}(X^\ell)\},$$

with $W^\ell$ the weight of $X^\ell$ at level $\varepsilon_\ell$; it stops when $\varepsilon_\ell=0$. Two functionals organize the analysis: $\mathcal J(X,W)=\tfrac12(\|W^{1/2}X\|_F^2+\|W^{-1/2}\|_F^2)$, of which IRLS-M is an alternating minimization, and $\mathcal J_\varepsilon(X)=\sum_{i=1}^n j^\varepsilon(\sigma_i(X))$ with $j^\varepsilon(u)=|u|$ for $|u|\ge\varepsilon$ and $(u^2+\varepsilon^2)/(2\varepsilon)$ otherwise.

Formalization targets

Goal: Theorem 6.11

For $\gamma=1/n$, any $K$, a surjective $\mathcal S$ and any run $(X^\ell,\varepsilon_\ell)$:

$$\text{(i)}\quad \mathcal S\ \text{SRNSP of order }K,\ \varepsilon_\ell\to0\ \Longrightarrow\ X^\ell\to\bar X,\ \operatorname{rank}\bar X\le K,\ \bar X=\text{the unique nuclear norm minimizer.}$$

(ii) If $\varepsilon_\ell\to\varepsilon>0$, the iterates are relatively compact, their accumulation points minimize $\mathcal J_\varepsilon$ on the feasible set, and the sequence converges when that minimizer is unique; under the SRNSP with $\eta<1-2/(K-2)$, every accumulation point $\bar X$ satisfies, for every feasible $X$ and $k<K-2\eta/(1-\eta)$,

$$\|X-\bar X\|_*\le\Lambda\rho_k(X)_*,\qquad\Lambda=\frac{4(1+\eta)^2}{(1-\eta)^2((K-k)(1-\eta)-2\eta)}+\frac{2(1+\eta)}{1-\eta}.$$

(iii) Under the same SRNSP, if a feasible matrix of rank at most $k$ exists, then $\varepsilon_\ell\to0$.

Milestones

In attack order: the weighted least squares step (Lemma 5.1, the optimality condition (5.4)); the weight step (Lemma 5.2, Proposition 5.3); monotonicity of $\mathcal J$ along the run (Proposition 6.1); singular value facts (Weyl's Theorem 7.1, attainment of $\rho_k$ at the spectral truncation, Lemma 6.10, Proposition 7.2); null space theory (Theorem 6.3, the inverse triangle inequality Lemma 6.6 with (6.5), Corollary 6.7); and the two steps of the proof of (ii), the optimality condition (6.10) for $\mathcal J_\varepsilon$ and the bound (6.11).

Significance

Theorem 6.11 is the convergence guarantee of IRLS-M. Combined with the fact that a small rank restricted isometry constant implies the SRNSP (Proposition 6.8, the companion mission), it yields Proposition 2.1 of the paper: under $\delta_{4K}<\sqrt2-1$, IRLS-M recovers every rank-$k$ matrix exactly and approximately low-rank matrices stably. Part (iii) says that the algorithm detects exact low-rank data on its own: the smoothing parameter must vanish.

The result is proved on paper; no machine-checked proof exists. A complete formalization would give a machine-checked convergence proof of an IRLS-type method; none is on the platform, for vectors or matrices. It also produces reusable matrix analysis: Weyl's perturbation bound for singular values, the nuclear norm best rank-$k$ approximation (a Mirsky-type theorem), additivity of the nuclear norm under orthogonality, the null space characterization of nuclear norm recovery, and optimality conditions for spectral functions.

Difficulty

Two steps resist the obvious argument. First, the weight update is a constrained minimization over the positive definite cone; identifying its solution (Proposition 5.3) requires a duality or spectral argument rather than setting a gradient to zero, because the constraint $W\preceq\varepsilon^{-1}I$ is active on small singular values. Second, in case (ii) the limit functional $\mathcal J_\varepsilon$ is convex but not strictly convex, so accumulation points cannot be pinned down by uniqueness; the analysis must instead pass the optimality condition (5.4) of the iterates to the limit, using continuity of the weights in the iterate, and derive (6.10). The step relating $\nabla\mathcal J_\varepsilon$ to $W\bar X$ needs the differentiability of unitarily invariant spectral functions, which the paper imports from Lewis and Sendov. Weyl's inequality and the spectral truncation facts, routine on paper, are not yet in Mathlib for rectangular matrices.

Formalization scope

All matrices are real (Matrix (Fin n) (Fin p) ℝ); the paper treats real and complex matrices alike. The paper's standing assumption $n\le p$ is a hypothesis wherever $n\times n$ objects ($XX^{\mathsf T}$, $W$, $\gamma=1/n$, $\mathcal J_\varepsilon$) occur. Nuclear norm, Frobenius norm, trace inner product and singular values come from the published definition HighDimStat_MatrixRank_Core; sv X i is $\sigma_{i+1}(X)$, 0-based. The measurement map is given by measurement matrices (observationOp), which represents every linear map to $\mathbb R^m$. The weight is defined with Mathlib's continuous functional calculus, and $W^{1/2}$ is cfc Real.sqrt W. The algorithm is the relation IsRun: each $X^{\ell+1}$ is some minimizer of (2.9), $X^0$ is free, and $\varepsilon_j=0$ after a stop. Accumulation points are MapClusterPt; uniqueness of a nuclear norm minimizer is a strict inequality against every other feasible matrix.

The goal cannot be satisfied vacuously: IsRun has a run for every surjective $\mathcal S$ and every $\mathscr M$ (Lemma 5.1 supplies the minimizers), it carries no positivity or uniqueness assumption a real run could violate, and the theorem keeps all three parts, including the unique-minimizer clause of (i) and the error bound of (ii) for every feasible $X$ and every admissible $k$.

Two printed slips are corrected and disclosed: (5.5) omits the factor $\tfrac12$ of (5.1), and (6.5) reverses the bracket of (6.4) at $\rho_k=0$. Contributions welcome: Weyl's inequality and the Mirsky-type truncation theorem for rectangular matrices, the spectral calculus behind Propositions 5.3 and (6.10), and proofs of the null space results, which are independent of the algorithm.

Selected references

• M. Fornasier, H. Rauhut, R. Ward, Low-rank matrix recovery via iteratively reweighted least squares minimization, SIAM J. Optim. 21(4), 2011. https://arxiv.org/abs/1010.2471 (v4 is the version formalized)
• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835
• B. Recht, W. Xu, B. Hassibi, Null space conditions and thresholds for rank minimization, Math. Program. 127, 2011. https://doi.org/10.1007/s10107-010-0422-2
• I. Daubechies, R. DeVore, M. Fornasier, C. S. Güntürk, Iteratively reweighted least squares minimization for sparse recovery, Comm. Pure Appl. Math. 63(1), 2010. https://doi.org/10.1002/cpa.20303
• K. Mohan, M. Fazel, Iterative reweighted least squares for matrix rank minimization, Proc. Allerton Conference, 2010; journal version Iterative reweighted algorithms for matrix rank minimization, JMLR 13, 2012. https://jmlr.org/papers/v13/mohan12a.html
• 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
• J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://doi.org/10.1137/080738970
• A. S. Lewis, H. S. Sendov, Nonsmooth analysis of singular values. I: Theory, Set-Valued Analysis 13(3), 2005. https://doi.org/10.1007/s11228-004-7197-7

Motivation

The eigenvalues of a large non-Hermitian random matrix are hard to study directly. For Hermitian matrices, the empirical spectral distribution (ESD) is controlled by the resolvent and the Stieltjes transform, both stable under small perturbations. For non-Hermitian matrices no such tool exists: eigenvalues can move a long way under tiny perturbations, and the moment method fails because moments do not determine a measure on $\mathbb C$. The route that works, going back to Girko (1984) and used by Bai (1997), Götze–Tikhomirov (2007), Pan–Zhou (2007) and Tao–Vu (2008), passes through logarithmic determinants. The identity $\frac1n\log|\det(A-zI)|=\int\log|w-z|\,d\mu_A(w)$ links the ESD $\mu_A$ to a scalar quantity. That scalar is computable from the singular values of $A-zI$, which are eigenvalues of a Hermitian matrix.

Tao and Vu, with an appendix by Krishnapur (Ann. Probab. 38 (2010) 2023–2065), turn this link into an exact criterion. Theorem 1.15 of that paper states that the ESD of a normalized i.i.d. random matrix converges to a measure $\mu$ if and only if the normalized log-determinants converge to the logarithmic potential of $\mu$ for almost every $z$. The same holds for a regularized version built from the singular values. This mission formalizes Theorem 1.15 and the main steps of its proof (§8 and Appendix A of the published article).

Setting

Let $x$ be a complex random variable with $\mathbf E x=0$ and $\mathbf E|x|^2=1$, and let $(x_{ij})_{i,j\ge1}$ be independent copies of $x$ on a probability space $(\Omega,\mathbf P)$. For each $n$, $X_n=(x_{ij})_{1\le i,j\le n}$. Let $M_n$ be deterministic $n\times n$ complex matrices with

$$\text{(1.3)}\qquad\sup_n\frac1{n^2}\|M_n\|_2^2<\infty,\qquad\|M\|_2^2=\sum_{i,j}|m_{ij}|^2,$$

and put $A_n=M_n+X_n$.

For $A\in M_n(\mathbb C)$ with eigenvalues $\lambda_1,\dots,\lambda_n$, counted with algebraic multiplicity, the ESD is $\mu_A=\frac1n\sum_i\delta_{\lambda_i}$. Its singular values are $\sigma_1(A)\ge\dots\ge\sigma_n(A)\ge0$. A sequence of random measures $\mu_n$ converges in probability to a deterministic $\mu$ if, for every continuous compactly supported $f:\mathbb C\to\mathbb R$, $\int f\,d\mu_n-\int f\,d\mu$ tends to $0$ in probability. It converges almost surely if, with probability one, $\int f\,d\mu_n\to\int f\,d\mu$ for all such $f$ at once. The logarithmic potential of a measure $\mu$ is $z\mapsto\int\log|w-z|\,d\mu(w)$.

Hypothesis (1.4) states that, for almost every $z$, the ESDs of the deterministic matrices $(\frac1{\sqrt n}M_n-zI)(\frac1{\sqrt n}M_n-zI)^*$ converge to a limit.

In Lean everything lives in the namespace UnivESD.LogDet. The ESD is esd, the one-based singular value is sv, logPotential is the logarithmic potential, and ConvInProb/ConvAS/ESDConvInProb/ESDConvAS are the modes of convergence. IIDArray is the entry model, HSBound is (1.3), shiftA M xs z n ω is $\frac1{\sqrt n}A_n-zI$, and Cond14 is (1.4).

Formalization targets

Goal: Theorem 1.15

Let $\mu$ be a probability measure on $\mathbb C$ with $\int|z|^2\,d\mu<\infty$. The following are equivalent:

1. $\mu_{\frac1{\sqrt n}A_n}\to\mu$ in probability;
2. for a.e. $z$, $\displaystyle\frac1n\log\Big|\det\big(\tfrac1{\sqrt n}A_n-zI\big)\Big|\to\int_{\mathbb C}\log|w-z|\,d\mu(w)$ in probability;
3. for a.e. $z$ there are $\varepsilon_n>0$, $\varepsilon_n\to0$, with

$$\frac1n\log\det\Big(\big(\tfrac1{\sqrt n}A_n-zI\big)\big(\tfrac1{\sqrt n}A_n-zI\big)^*+\varepsilon_nI\Big)\to2\int_{\mathbb C}\log|w-z|\,d\mu(w)$$

in probability.

Under (1.4) the same equivalence holds with almost sure convergence throughout.

Milestones, in the order the proof uses them

• (8.1): for a.e. $z$, $w\mapsto\log|w-z|$ is $\mu$-integrable.
• Lemma A.3 (Weyl's comparison for products): $\prod_{j\le J}|\lambda_j|\le\prod_{j\le J}\sigma_j(A)$ and $\prod_{j\ge J}\sigma_j(A)\le\prod_{j\ge J}|\lambda_j|$.
• (8.3): $\mathbf P(\sigma_{n-i}\le ci/n)=O(\exp(-n^{0.01}))$ for $2n^{0.99}\le i\le n-1$.
• (8.2): $\frac1n\sum_{i=1}^n\big(\log\sqrt{\sigma_i^2+\varepsilon_n}-\log\sigma_i\big)\to0$ almost surely.
• p. 2057: almost surely, eventually, $\frac1n\sum_{(1-\kappa)n<i\le n}\log\frac1{\sigma_i}\le O(\kappa\log\frac1\kappa)$, and the same bound for $\log\frac1{|\lambda_i|}$.

Significance

Theorem 1.15 reduces convergence of a non-Hermitian ESD to a family of scalar limit statements. Each of these can be attacked through Hermitian tools, because the regularized log-determinant in (iii) is a smooth functional of the singular values. Corollary 1.16 of the paper derives from it a practical criterion: the ESD converges to $\mu$ once the singular value distributions of $\frac1{\sqrt n}A_n-zI$ converge for a.e. $z$ to laws $\eta_z$ with $\int\log t\,d\eta_z=2\int\log|w-z|\,d\mu$. With the universality principle (Theorem 1.5, the companion mission) and Mehta's computation for complex Gaussian matrices, this yields the circular law for i.i.d. matrices with finite variance.

The theorem is proved in the source. To our knowledge neither it nor any of its milestones has a machine-checked proof. Mathlib has the ingredients for the objects (characteristic polynomials and their roots, LinearMap.singularValues, the strong law of large numbers) but not the results. A formal proof would give the platform its first verified bridge between eigenvalue and singular value asymptotics. Lemma A.3 alone, Weyl's multiplicative majorization, is a standard linear-algebra fact absent from Mathlib.

Difficulty

Two things make the obvious argument fail. First, $\log$ is unbounded at $0$. Vague convergence of $\mu_{\frac1{\sqrt n}A_n}$ controls $\int f\,d\mu_n$ only for continuous compactly supported $f$, while $\log|w-z|$ has a singularity at $w=z$ and grows at infinity. Passing between (i) and (ii) therefore requires uniform control of the eigenvalues (and singular values) near $0$ after the shift: the contribution of the smallest ones must vanish. Second, eigenvalues are not stable under perturbation, so this control cannot be read off the eigenvalues. It has to come from the singular values, through a lower-tail bound on $\sigma_{n-i}$ that is exponentially small in a power of $n$, and through a deterministic inequality transferring bounds from singular values to eigenvalues. The smallest singular values ($i$ below $n^{0.99}$) need a separate polynomial lower bound (the paper's Lemma 4.1, posed in the companion mission). The tail bound in its printed form is false at that end of the range.

Formalization scope

Conventions committed to in Lean:

• The ESD is $n^{-1}$ times the sum of Dirac masses over the root multiset of the characteristic polynomial, so multiplicities are kept. Test functions are real-valued, continuous and compactly supported. Almost sure ESD convergence uses one null set for all test functions.
• The matrices $X_n$ are the top-left corners of one infinite i.i.d. array. In-probability statements do not depend on how the $X_n$ are coupled across $n$, but almost-sure statements do, and the paper's proof applies the strong law to this array. The limit in (1.4) is required to be a probability measure, which is equivalent under (1.3).
• The second-moment condition on $\mu$ is Integrable (‖w‖²) μ. The logarithmic potential is a Bochner integral, which is $0$ when not integrable; by (8.1) this happens only for a null set of $z$, which "for a.e. $z$" ignores.
• Real.log 0 = 0. In (ii), a singular matrix would contribute $0$ instead of $-\infty$; for this model the determinant is almost surely nonzero eventually. Every milestone with $\log\sigma_i$ or $\log|\lambda_i|$ carries positivity of those quantities in its conclusion.
• Singular values are one-based (sv A i is Mathlib's singularValues (i-1)). Eigenvalue enumerations are Fin n-indexed, and the paper's $\lambda_i$ is index $i-1$.
• The paper's $O(\cdot)$ constants are existential and fixed before $n$. In the $\kappa\log(1/\kappa)$ bounds the constant is fixed before $\kappa$; a $\kappa$-dependent constant would make the bounds empty.

Disclosed corrections to the printed text:

1. (iii)'s matrix. Theorem 1.15 prints a mis-bracketed product, and (1.8) prints $(C+\varepsilon_nI)(C^*+\varepsilon_nI)$. The Lean uses $CC^*+\varepsilon_nI$ with $C=\frac1{\sqrt n}A_n-zI$, the matrix of (8.2) and of the proof of Corollary 1.16.
2. (8.3)'s range. It is printed for $1\le i\le n-n^{0.99}$, which is false for small $i$: for Gaussian entries and $M_n=0$, $n\sigma_{n-1}$ has a non-degenerate limit law. It is posed on $2n^{0.99}\le i\le n-1$, the range the proof covers and the use needs.
3. Lemma A.3, second inequality. It is posed for $1\le J\le n$, since $\sigma_0$ is undefined. The eigenvalues are ordered $|\lambda_1|\ge\dots\ge|\lambda_n|$, not $|\lambda_1|\le\dots\le|\lambda_n|$ as printed: the printed order is a slip. With it, both inequalities are weaker than Weyl's and cannot support the use on p. 2057, which orders the eigenvalues decreasingly. The decreasing order implies the printed form.
4. (8.2) and (8.1). (8.2) is stated for every deterministic $\varepsilon_n>0$ with $\varepsilon_n\to0$; the proof uses nothing else. (8.1) is stated as $\mu$-integrability plus local integrability of $z\mapsto\int|\log|w-z||\,d\mu(w)$.

A trivializing formalization is ruled out by construction. The goal mentions only $A_n$ and $\mu$. The proof's comparison ensemble $B_n=\sqrt n\,\mathrm{diag}(\lambda_i)$ is not a hypothesis. No statement takes a log-potential or a log-determinant as an input that could be fixed to make it hold.

The companion mission (Theorem 1.5, universality) poses Theorem 2.1 (the replacement principle), Lemma 1.7 (tightness) and Lemma 4.1 (least singular value), which the proof here also uses. They are not restated here. Once that mission is published they belong here as references. Contributions are welcome on the linear-algebra layer (Lemma A.3, multiplicative Weyl majorization), the Fubini argument of (8.1), and the singular-value tail bound (8.3). These are reusable well beyond this paper.

Selected references

• T. Tao, V. Vu (appendix by M. Krishnapur), Random matrices: Universality of ESDs and the circular law, Ann. Probab. 38(5) (2010) 2023–2065. https://doi.org/10.1214/10-AOP534 (source of this mission; published version).
• V. L. Girko, The circular law, Teor. Veroyatnost. i Primenen. 29 (1984) 669–679. https://doi.org/10.1137/1129095
• Z. D. Bai, Circular law, Ann. Probab. 25(1) (1997) 494–529. https://doi.org/10.1214/aop/1024404298
• F. Götze, A. Tikhomirov, The circular law for random matrices, Ann. Probab. 38(4) (2010) 1444–1491. https://doi.org/10.1214/09-AOP522
• T. Tao, V. Vu, Random matrices: the circular law, Commun. Contemp. Math. 10(2) (2008) 261–307. https://doi.org/10.1142/S0219199708002788
• H. Weyl, Inequalities between the two kinds of eigenvalues of a linear transformation, Proc. Natl. Acad. Sci. USA 35 (1949) 408–411. https://doi.org/10.1073/pnas.35.7.408