Linear algebra

Motivation

Nuclear norm minimization is the standard convex surrogate for rank minimization: to recover a low-rank matrix from a few linear measurements, or from a subset of its entries, one minimizes the sum of the singular values subject to the data constraints. For matrix completion, Candès and Recht (Found. Comput. Math. 2009) showed that this convex program recovers a low-rank matrix exactly from sufficiently many random entries. Solving it at scale is another matter: interior-point methods for the equivalent semidefinite program become impractical beyond matrices of a few hundred rows and columns.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm, whose iterates are cheap and typically of low rank. SVT does not solve the nuclear norm problem itself. It solves a proximal problem, in which the nuclear norm is replaced by $\tau\|X\|_* + \tfrac12\|X\|_F^2$ for a fixed parameter $\tau>0$. Section 3.4 of the paper justifies this substitution: as $\tau\to\infty$, the solutions of the proximal problem converge to a specific solution of the nuclear norm problem, the one of least Frobenius norm. This mission formalizes that result, Theorem 3.1 of the paper, under general convex constraints.

Setting

Let $n_1, n_2$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the space of real $n_1\times n_2$ matrices, with the inner product $\langle X, Y\rangle = \operatorname{trace}(X^*Y) = \sum_{i,j}X_{ij}Y_{ij}$. Three functions of a matrix $X$ are used:

• the Frobenius norm $\|X\|_F = \sqrt{\langle X, X\rangle}$;
• the nuclear norm $\|X\|_*$, the sum of the singular values of $X$;
• for a parameter $\tau$, the proximal objective $f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2$.

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be constraint functions and $\mathcal C = \{X : f_i(X)\le 0,\ i = 1,\dots,m\}$ the feasible set. The nuclear norm problem is

$$\text{(1.6)}\qquad \text{minimize } \|X\|_* \quad \text{subject to } f_i(X)\le 0,\ i=1,\dots,m,$$

and, for $\tau>0$, the proximal problem is

$$\text{(3.4)}\qquad \text{minimize } f_\tau(X) \quad \text{subject to } f_i(X)\le 0,\ i=1,\dots,m.$$

When the $f_i$ are convex and $\mathcal C$ is nonempty, (3.4) has exactly one solution, written $X^\star_\tau$, because $f_\tau$ is strongly convex. Problem (1.6) may have many solutions. Among them, the paper singles out the minimum Frobenius norm solution

$$\text{(3.14)}\qquad X_\infty := \arg\min_X\{\|X\|_F^2 : X \text{ is a solution of (1.6)}\}.$$

Linear equality constraints, and in particular the matrix completion constraints $X_{ij} = M_{ij}$ for sampled entries $(i,j)$, are covered by taking pairs of affine functionals.

Formalization targets

Goal: Theorem 3.1

Assume that the $f_i$ are convex and lower semicontinuous. Then

$$\text{(3.15)}\qquad \lim_{\tau\to\infty}\|X^\star_\tau - X_\infty\|_F = 0.$$

Milestones

In the order in which the paper's proof uses them (all on p. 1967):

1. Eq. (3.16), for every $\tau>0$:

$$\|X^\star_\tau\|_* + \frac{1}{2\tau}\|X^\star_\tau\|_F^2 \le \|X_\infty\|_* + \frac{1}{2\tau}\|X_\infty\|_F^2 \quad\text{and}\quad \|X_\infty\|_*\le\|X^\star_\tau\|_*.$$

2. Eq. (3.17), for every $\tau>0$: $\|X^\star_\tau\|_F^2 \le \|X_\infty\|_F^2$.
3. Convergence of the nuclear norms: $\lim_{\tau\to\infty}\|X^\star_\tau\|_* = \|X_\infty\|_*$.
4. Uniqueness of $X_\infty$: two minimum Frobenius norm solutions of (1.6) coincide when the $f_i$ are convex.
5. Cluster points: if $\tau_k\to\infty$ and $X^\star_{\tau_k}\to X_c$, then $X_c = X_\infty$.

Significance

The result itself. Theorem 3.1 is the link between the problem SVT actually solves and the problem one wants solved. The companion missions of this series prove that the SVT iteration, and its variant for general convex constraints, converges to $X^\star_\tau$. Theorem 3.1 says what $X^\star_\tau$ is worth: for large $\tau$ it is close to a nuclear norm minimizer, and the minimizer it approaches is identified exactly, namely the one of least Frobenius norm. The statement is not specific to matrix completion. It covers every finite family of convex, lower semicontinuous constraints, and hence noisy variants such as the inequality-constrained problems of §3.3 of the paper.

Formalizing it. The theorem is proved in the paper, in about half a page. It has not, to our knowledge, been machine-checked. A formal proof pins down the hypotheses: the argument needs the minimizers to exist, and it uses continuity and convexity of the nuclear norm, closedness of the feasible set, and uniqueness of $X_\infty$. It also produces a reusable fact about the nuclear norm in Lean, namely that the sum of singular values is a continuous convex function of the matrix.

Difficulty

The first steps are elementary consequences of the definitions of $X^\star_\tau$ and $X_\infty$: (3.16) compares objective values, and (3.17) and the convergence of the nuclear norms follow by algebra and a squeeze. The difficulty lies elsewhere.

• Identifying the limit. Boundedness gives cluster points of $X^\star_\tau$, not convergence. Each cluster point must be shown to be feasible, to be optimal for (1.6), and to have the least Frobenius norm among the optimal points. Feasibility uses lower semicontinuity of the constraints. Optimality uses continuity of the nuclear norm. Minimality uses (3.17) passed to the limit.
• Uniqueness of $X_\infty$. The last step concludes $X_c = X_\infty$ from $\|X_c\|_F = \|X_\infty\|_F$, which needs uniqueness of the minimum Frobenius norm solution. That in turn needs convexity of the solution set of (1.6), hence convexity of the nuclear norm, together with strict convexity of $\|\cdot\|_F^2$.
• Nuclear norm in Lean. The nuclear norm is defined from singular values, and its convexity (the triangle inequality for the sum of singular values) and continuity are not currently available as ready-made statements. They are the main groundwork.

A tempting shortcut, reading the family $X^\star_\tau$ as a sequence indexed by integers, proves a weaker statement: the limit in (3.15) is over real $\tau\to\infty$.

Formalization scope

• Matrices. Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, abbreviated Mat n₁ n₂, over the reals as in the paper. $\langle X,Y\rangle = \sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F = \sqrt{\langle X,X\rangle}$.
• Nuclear norm. $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X. It is the genuine sum of singular values, not an abstract norm or the Frobenius norm.
• Constraints. The constraints are a family f : Fin m → Mat n₁ n₂ → ℝ of real-valued functions. $m = 0$ (no constraints) is allowed.
• Hypotheses of Theorem 3.1. The hypotheses are ConvexOn ℝ Set.univ (f i) and LowerSemicontinuous (f i) for every $i$. Lower semicontinuity is redundant for real-valued convex functions on a finite-dimensional space, but it is kept because the theorem states it.
• $X^\star_\tau$ and $X_\infty$. $X^\star_\tau$ is a family Xτ : ℝ → Mat n₁ n₂ assumed to solve (3.4) for every $\tau>0$, and its values at $\tau\le 0$ play no role. $X_\infty$ is a matrix assumed to satisfy the defining property (3.14): it solves (1.6) and has the least $\|\cdot\|_F^2$ among its solutions. Uniqueness of $X_\infty$ is a milestone to prove, not an assumption.
• Vacuous case. These hypotheses presuppose, as the paper does, that (1.6) has a solution. They can be met exactly when the feasible set is nonempty. When it is empty the statement is vacuous, which matches the paper, where $X_\infty$ is then undefined.
• Limits and topology. Limits in $\tau$ are along Filter.atTop on $\mathbb R$. Convergence of matrices uses Mathlib's entrywise topology, which is the topology of $\|\cdot\|_F$. The goal states (3.15) literally, with the Frobenius norm of the difference tending to $0$.
• Excluded shortcuts. A formalization that replaces the nuclear norm by the Frobenius norm or by an arbitrary norm, indexes $\tau$ by $\mathbb N$, or assumes uniqueness or convergence as a hypothesis would not be Theorem 3.1. It is ruled out.

Infrastructure. The needed facts, all reusable beyond this mission:

• nonnegativity, convexity and continuity of the nuclear norm on real matrices;
• closedness and convexity of sublevel sets of convex lower semicontinuous functions;
• uniqueness of the minimizer of a strictly convex function over a convex set;
• a cluster-point argument for bounded families in finite-dimensional spaces.

Contributions of these general lemmas as separate theorems are welcome.

Selected references

• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Rev. 52(3):471–501, 2010. https://doi.org/10.1137/070697835

Motivation

Singular value thresholding (SVT) is a first-order method introduced by Cai, Candès and Shen (SIAM J. Optim. 20 (2010)) for recovering a low-rank matrix from incomplete or indirect information. Its basic form, for matrix completion, alternates a soft-thresholding of singular values with a gradient step on a dual variable, and needs only one sparse singular value decomposition per iteration. That is what made nuclear-norm heuristics usable on matrices with tens of thousands of rows and columns, where interior-point methods for the equivalent semidefinite program do not fit in memory.

Matrix completion is only one constraint set. In applications the data are noisy linear measurements $b = \mathcal A(M) + z$, and the constraint takes the form of componentwise error bounds or norm balls around the data (§3.3 of the paper). Section 3.2 of the paper extends the method to a general finite family of convex constraints, and §4.2 proves that the extended iteration converges. This mission formalizes that extension and its convergence theorem, Theorem 4.4.

Setting

Let $n_1, n_2, m$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the real $n_1\times n_2$ matrices, with the Frobenius inner product $\langle X, Y\rangle = \sum_{i,j} X_{ij}Y_{ij}$ and norm $\|X\|_F = \sqrt{\langle X, X\rangle}$. The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$. For a fixed $\tau > 0$ the objective is

$$f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2 .$$

A matrix $Z$ is a subgradient of a function $g$ at $X_0$, written $Z\in\partial g(X_0)$, if $g(X)\ge g(X_0) + \langle Z, X - X_0\rangle$ for all $X$.

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be convex and put $\mathcal F(X) = (f_1(X),\dots,f_m(X))\in\mathbb R^m$. On $\mathbb R^m$, $\langle u, v\rangle = \sum_i u_iv_i$ and $\|v\|$ is the Euclidean norm. The constrained problem is

$$\text{(3.4)}\qquad \text{minimize } f_\tau(X)\quad\text{subject to } f_i(X)\le 0,\ i=1,\dots,m,$$

with Lagrangian $\mathcal L(X, y) = f_\tau(X) + \langle y, \mathcal F(X)\rangle$ for $y\ge 0$. A pair $(X^\star, y^\star)$ with $y^\star\ge0$ is primal-dual optimal if it is a saddle point:

$$\mathcal L(X^\star, y)\le \mathcal L(X^\star, y^\star)\le \mathcal L(X, y^\star)\qquad\text{for all } y\ge 0,\ X .$$

The paper's standing assumption "strong duality holds" is the existence of such a pair.

The iteration (3.5) starts from $y^0 = 0$ and, for step sizes $\delta_k$, sets for $k = 1, 2, \dots$

$$X^k = \arg\min_X\{f_\tau(X) + \langle y^{k-1}, \mathcal F(X)\rangle\},\qquad y^k = [\,y^{k-1} + \delta_k\mathcal F(X^k)\,]_+ ,$$

where $x_+$ has entries $\max(x_i, 0)$. It is Uzawa's method for (3.4): an exact minimization in the primal variable followed by a projected ascent step on the dual. When $\mathcal F(X) = b - \mathcal A(X)$ is affine, the minimization is a singular value thresholding step, which gives the algorithm its name.

The analysis of §4.2 assumes $\mathcal F$ is Lipschitz in the sense

$$\text{(4.2)}\qquad \|\mathcal F(X) - \mathcal F(Y)\|\le L\,\|X - Y\|_F\quad\text{for all } X, Y,$$

for a constant $L\ge 0$.

Formalization targets

Goal: Theorem 4.4 (p. 1969)

If $0 < \inf_k\delta_k\le\sup_k\delta_k < 2/L^2$ and strong duality holds, then the sequence $X^k$ of (3.5) converges to the unique solution of (3.4):

$$\exists!\,X^\star\ \text{solving (3.4)},\qquad \lim_{k\to\infty} X^k = X^\star .$$

Milestones, in the order the proof uses them

• Lemma 4.1 (p. 1968): $\langle Z - Z', X - X'\rangle\ge\|X - X'\|_F^2$ for $Z\in\partial f_\tau(X)$, $Z'\in\partial f_\tau(X')$.
• Lemma 4.3 (p. 1969): for a primal-dual optimal pair and each $\delta > 0$, $y^\star = [y^\star + \delta\mathcal F(X^\star)]_+$.
• Eq. (4.4) (p. 1969): there are $Z^k\in\partial f_\tau(X^k)$ and $Z^\star\in\partial f_\tau(X^\star)$ with $\langle Z^k, X - X^k\rangle + \langle y^{k-1}, \mathcal F(X) - \mathcal F(X^k)\rangle\ge 0$ and $\langle Z^\star, X - X^\star\rangle + \langle y^\star, \mathcal F(X) - \mathcal F(X^\star)\rangle\ge 0$ for all $X$.
• Eq. (4.5) (p. 1969): $\langle y^{k-1} - y^\star, \mathcal F(X^k) - \mathcal F(X^\star)\rangle\le -\|X^k - X^\star\|_F^2$.
• Contraction step (p. 1969): $\|y^k - y^\star\|\le\|y^{k-1} - y^\star + \delta_k(\mathcal F(X^k) - \mathcal F(X^\star))\|$.
• Eq. (4.6) (p. 1970): if $2\delta_k - \delta_k^2L^2\ge\beta > 0$ for $k\ge1$, then $\|y^k - y^\star\|^2\le\|y^{k-1} - y^\star\|^2 - \beta\|X^k - X^\star\|_F^2$.

Significance

The result. Theorem 4.4 is the convergence guarantee for SVT beyond matrix completion. The componentwise error bounds of (3.8), whose SVT iteration is (3.9), are finitely many affine constraints and fall under it directly, as does any finite family of Lipschitz convex constraints, for instance a Frobenius-norm ball around the data. The conic variants of §3.3 ((3.11)–(3.13)) project the dual variable onto a cone rather than onto the nonnegative orthant and are not covered by the theorem as stated. Together with Theorem 3.1 of the same paper, which says that the solution of (3.4) tends to the minimum-nuclear-norm solution as $\tau\to\infty$, it justifies using SVT as a solver for nuclear-norm minimization under general convex constraints.

Formalizing it. The theorem is proved in the paper, with two steps delegated to the literature: Lemma 4.3 cites [31], and the concluding step reads "the conclusion is as before". Its proof is short but relies on convex-analytic facts that are standard on paper and missing, in this form, from Mathlib: subgradients of the nuclear norm, the subdifferential sum rule for finite convex functions, and nonexpansiveness of the projection onto the nonnegative orthant. No machine-checked proof of this theorem or of Uzawa-type convergence for nuclear-norm objectives is known to exist. The mission produces a complete, checked version of the argument, including the omitted closing step.

Difficulty

The obvious approach is to view (3.5) as projected gradient ascent on the dual function $g(y) = \min_X\mathcal L(X, y)$ and quote the standard convergence theorem for gradient methods with Lipschitz gradients. That does not apply directly: for general convex $f_i$ the dual function need not be differentiable, $\mathcal F(X^k)$ is only a supergradient, and the Lipschitz hypothesis (4.2) is on $\mathcal F$, not on a dual gradient. The proof instead works with the primal-dual pair: it needs first-order optimality conditions (4.4), which require a subdifferential sum rule for $f_\tau + \sum_i y_i f_i$ with nonsmooth $f_i$, and it needs the strong monotonicity of $\partial f_\tau$ (Lemma 4.1), which depends on the description of subgradients of the nuclear norm. A second subtlety is that the theorem asserts convergence of the whole primal sequence to the unique solution, not to some solution along a subsequence, while nothing is claimed about convergence of the dual sequence.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, vectors in $\mathbb R^m$ are Fin m → ℝ, and convergence of matrices is in Mathlib's product topology, which coincides with the Frobenius topology. The nuclear norm is the sum of Mathlib's LinearMap.singularValues of the matrix viewed as a map between Euclidean spaces. Each $f_i$ is a real-valued function with ConvexOn ℝ Set.univ. The iteration is a predicate on sequences indexed by ℕ: the paper's step $k$ produces X (k+1) and y (k+1) from y k with step size δ (k+1), and y 0 = 0. $X^k$ is required to minimize $\mathcal L(\cdot, y^{k-1})$; for $\tau>0$ and convex $f_i$ this minimizer exists and is unique, so the predicate is satisfiable and determines the sequence. The step-size condition is stated as $a\le\delta_k\le C$ for $k\ge1$ with $a>0$ and $C L^2 < 2$, which avoids the division $2/L^2$ (evaluated as $0$ in Lean when $L=0$); for $L=0$ it requires only bounded steps, matching the convention $2/0 = \infty$. Strong duality is the hypothesis that a saddle point exists; Slater's condition is not assumed. The paper's standing assumptions ($\tau>0$, convex $f_i$, and (4.2) where $L$ enters) appear as explicit hypotheses in every statement.

A formalization that assumes convergence or boundedness of the dual iterates, replaces the primal minimization by a closed-form thresholding step (valid only for affine $\mathcal F$), or states only subsequential convergence would not be this theorem; each of these is excluded by the statements above.

A complete development needs: subgradients of the nuclear norm and strong monotonicity of $\partial f_\tau$; existence and characterization of minimizers of strongly convex continuous functions on a finite-dimensional space; the subdifferential sum rule for finite convex functions; complementary slackness from the saddle-point inequalities; and nonexpansiveness of the entrywise positive part. These are reusable beyond this mission, especially for other Uzawa and augmented Lagrangian analyses. Contributions of any of these pieces as separate lemmas are welcome.

Selected references

• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Nonlinear Programming, Stanford University Press, 1958.
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441

Motivation

Matrix completion asks to recover an $n_1\times n_2$ matrix $M$ from a subset $\Omega$ of its entries. When $M$ has low rank, a standard convex surrogate is to minimize the nuclear norm $\|X\|_*$ (the sum of the singular values) subject to agreeing with $M$ on $\Omega$; Candès and Recht showed that this recovers $M$ exactly under incoherence and sampling conditions (Candès–Recht 2009). Generic interior-point solvers for this semidefinite program do not scale beyond matrices of a few hundred rows.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm: a first-order iteration whose only nonlinear step is a soft-thresholding of singular values, and whose other iterate is a sparse matrix supported on $\Omega$. The algorithm has become a standard baseline in low-rank matrix recovery and a model example of dual (Uzawa-type) methods for nuclear-norm problems. This mission formalizes its convergence theorem.

Setting

All matrices are real. For $X,Y\in\mathbb R^{n_1\times n_2}$ write $\langle X,Y\rangle=\operatorname{trace}(X^*Y)=\sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F^2=\langle X,X\rangle$. The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$.

For an index set $\Omega$, the sampling projector $P_\Omega$ keeps the entries with indices in $\Omega$ and sets the others to zero.

A reduced singular value decomposition of a matrix $Y$ of rank $r$ is $Y=U\Sigma V^*$ with $U$ ($n_1\times r$) and $V$ ($n_2\times r$) having orthonormal columns and $\Sigma=\operatorname{diag}(\sigma_1,\dots,\sigma_r)$ with $\sigma_i>0$. For $\tau\ge0$ the singular value shrinkage operator is

$$\mathcal D_\tau(Y)=U\operatorname{diag}\big((\sigma_i-\tau)_+\big)V^*,\qquad t_+=\max(0,t).$$

Fix $\tau>0$, a sequence of step sizes $\{\delta_k\}_{k\ge1}$ and data $M$. The SVT iteration (2.7) starts from $Y^0=0$ and sets, for $k=1,2,\dots$,

$$X^k=\mathcal D_\tau(Y^{k-1}),\qquad Y^k=Y^{k-1}+\delta_k P_\Omega(M-X^k).$$

The proximal problem (2.8) is

$$\text{minimize}\ \ f_\tau(X)=\tau\|X\|_*+\tfrac12\|X\|_F^2\quad\text{subject to}\ \ P_\Omega(X)=P_\Omega(M).$$

More generally, for a linear map $\mathcal A:\mathbb R^{n_1\times n_2}\to\mathbb R^m$ with adjoint $\mathcal A^*$ and spectral norm $\|\mathcal A\|=\sup\{\|\mathcal A(X)\|_{\ell_2}:\|X\|_F=1\}$, and $b\in\mathbb R^m$, problem (3.1) is to minimize $f_\tau(X)$ subject to $\mathcal A(X)=b$, and Uzawa's iteration (3.3) starts from $y^0=0$ and sets $X^k=\mathcal D_\tau(\mathcal A^*(y^{k-1}))$, $y^k=y^{k-1}+\delta_k(b-\mathcal A(X^k))$.

Formalization targets

Goal: Theorem 4.2, second sentence (p. 1968)

If $0<\inf_k\delta_k\le\sup_k\delta_k<2$, then (2.8) has a unique solution $X^\star$ and the SVT iterates satisfy

$$\lim_{k\to\infty}X^k=X^\star .$$

Theorem 4.2, first sentence (p. 1968)

If (3.1) is feasible and $0<\inf_k\delta_k\le\sup_k\delta_k<2/\|\mathcal A\|^2$, then (3.1) has a unique solution and the iterates $X^k$ of (3.3) converge to it.

Supporting results (milestones, in attack order)

1. Well-definedness of $\mathcal D_\tau$ (§2.1, p. 1960): the output does not depend on the chosen SVD.
2. Theorem 2.1 (p. 1960): $\mathcal D_\tau(Y)=\arg\min_X \tfrac12\|X-Y\|_F^2+\tau\|X\|_*$.
3. Sparsity of the iterates (§2.2, p. 1961): since $Y^0=0$, every $Y^k$ vanishes outside $\Omega$.
4. Eq. (2.14) (p. 1964): the minimizers of the Lagrangian $f_\tau(X)+\langle Y,P_\Omega(M-X)\rangle$ are those of $\tau\|X\|_*+\tfrac12\|X-P_\Omega Y\|_F^2$.
5. Lemma 4.1 (p. 1968): for $Z\in\partial f_\tau(X)$, $Z'\in\partial f_\tau(X')$, $\langle Z-Z',X-X'\rangle\ge\|X-X'\|_F^2$.
6. The §3.1 reduction (p. 1964): for a sampling operator, $\mathcal A^*\mathcal A=P_\Omega$ and (3.3) becomes (2.7) under $Y^k=\mathcal A^*(y^k)$.
7. Theorem 4.2, first sentence, as above.

Significance

The theorem certifies that SVT, run with any step sizes in a fixed interval $(0,2)$, computes the unique minimizer of the strongly convex surrogate (2.8). Together with the separate fact that the solution of (2.8) tends to the minimum nuclear norm completion as $\tau\to\infty$ (the paper's Theorem 3.1, a companion mission), this is what justifies using SVT as a solver for nuclear-norm matrix completion. Theorem 2.1, the proximal characterization of singular value soft-thresholding, is used throughout the literature on proximal methods for low-rank problems.

The paper's proof of Theorem 4.2 consists of the reduction to Uzawa's method and a citation of a general convergence theorem for projected gradient methods on the dual. The formalization produces a self-contained, machine-checked chain: the proximal characterization of $\mathcal D_\tau$, the Lagrangian identity, strong monotonicity of $\partial f_\tau$, and the convergence argument itself. To our knowledge none of these results has a machine-checked proof; Mathlib at the pinned revision has singular values of linear maps but no SVD structure, no nuclear norm and no subgradient calculus.

Difficulty

Nothing in the iteration is a gradient step of a smooth function in $X$: the $X$-update is a nonsmooth proximal map, and the convergence of $X^k$ is not visible from the recursion itself. The paper's argument cites a general theorem on projected gradient methods ([25, Theorem 2.1]) and takes for granted that "strong duality holds" for (2.8) (p. 1963), so the existence of a Lagrange multiplier is part of what must be formalized. Theorem 2.1 depends on the subdifferential of the nuclear norm, which Mathlib does not provide, and therefore on the singular value decomposition and the duality between the nuclear and spectral norms. Convergence of objective values or of a subsequence would not suffice: the target is convergence of the whole sequence $X^k$ to the unique solution.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ; convergence is Mathlib's topology on matrices, which coincides with the Frobenius-norm topology. $\langle\cdot,\cdot\rangle$ and $\|\cdot\|_F$ are defined entrywise; $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of $X$ viewed as a map $\mathbb R^{n_2}\to\mathbb R^{n_1}$. The shrinkage operator is a relation IsShrink τ Y X defined, as in (2.1)–(2.2), through some reduced SVD of $Y$; well-definedness is a milestone. It is not defined as the minimizer of (2.3), which would make Theorem 2.1 definitional. Linear maps $\mathcal A$ are given by matrices $A_1,\dots,A_m$ with $\mathcal A(X)_i=\langle A_i,X\rangle$, and a sampling operator by an injective enumeration of $\Omega$. Subgradients are those of (2.4).

Sequences are indexed by $\mathbb N$: Lean's step $k+1$ is the paper's step $k$, so $X^0$ and $\delta_0$ are unused. Committed conventions:

• $Y^0=0$ and $y^0=0$ are hypotheses; with a start that is nonzero outside $\Omega$ the iterates converge to a different matrix.
• The standing $\tau>0$ is kept, except in Theorem 2.1 and the well-definedness statement, which are printed for $\tau\ge0$.
• The step-size conditions are explicit bounds $a>0$, $C$ with $a\le\delta_k\le C$ for $k\ge1$, together with $C<2$, respectively $C\|\mathcal A\|^2<2$. The multiplicative form avoids Lean's $x/0=0$: for $\mathcal A=0$ the condition does not become unsatisfiable.
• Feasibility of (3.1) is an added hypothesis of Theorem 4.2's first sentence, since "the unique solution" presupposes it.
• "Converges to the unique solution" is stated as existence and uniqueness of the solution together with convergence of the whole sequence to it.

A small unprinted helper, $\|\mathcal A\|\le1$ for sampling operators, is included to pass from the first sentence of Theorem 4.2 to the second; it is not a milestone. The subdifferential formula (2.6) of the nuclear norm and the Fejér-type condition of §5.1.2 are not stated. Reusable infrastructure welcome from solvers: existence and uniqueness properties of the reduced SVD, the nuclear/spectral norm duality, the subdifferential of the nuclear norm, and a general convergence theorem for Uzawa's method with a strongly convex objective.

Selected references

• J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
• E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
• K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Non-Linear Programming, Stanford University Press, 1958.

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$, where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$, defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$, and $1\le n<m$. For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$, $W=\mathrm{diag}(w)$, $W^\alpha=\mathrm{diag}(w_i^\alpha)$, and $A_s=S^{-1}A$. For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$.

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$, and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .$$

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$, with $G(s)=\mathrm{diag}(g(s))$, $G'(s)$ the Jacobian of $g$ at $s$, and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$:

1. Size: $\|g(s)\|_1\le c_1$;
2. Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$;
3. Step consistency: $c_r\ge1$ and for all $r\ge c_r$, $y\in\mathbb R^m$: $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$;
4. Uniformity: $\|g(s)\|_\infty\le2$.

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$,

$$\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).$$

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

$$\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},$$

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$, and the resulting $g$ is a weight function with

$$c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .$$

Milestones: the three bullets of Theorem 1

• Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$.
• Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$.
• Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$.

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$-iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$-sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$. The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$, and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$) and $A^\top W^\alpha A$ (which defines $g$). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$, $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$-norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$, and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$, and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

• Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$).
• $1\le n<m$. $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
• Reading of $\alpha$: the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$, giving $\alpha\in(0,1)$.
• Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$, while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$).
• The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$.
• $g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$. Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — $U(1)$, $SU(2)$ and $SU(3)$ — from a single linear-algebra statement applied at three node sizes. A node carrying $n$ oscillator pairs has a $2n$-dimensional real state space with a complex structure $J$. Within the model, the couplings that do no net work (passive couplings) are the symmetric matrices, and those that respect $J$ are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly $n^2$, which is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ (Unitary group):

node size $n$	admissible dimension	Lie algebra
1	1	$\mathfrak{u}(1)$
2	4	$\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$
3	9	$\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$

The dimension count has so far been checked numerically for $n = 1, \dots, 5$ only, giving $1, 4, 9, 16, 25$. A machine-checked proof covers every $n$, and it is the claim a physicist examining the model would check first.

What this mission does NOT prove. This mission proves the linear algebra: symmetric matrices commuting with $J$ form a space of dimension $n^2$. It does not prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it.

Setting

Fix a natural number $n$. Consider real $2n \times 2n$ matrices, with rows and columns indexed by two copies of $\{0, \dots, n-1\}$, so that each matrix is written in $2 \times 2$ block form with $n \times n$ blocks:

$$W = \begin{pmatrix} A & B \\ C & D \end{pmatrix}.$$

Let $I$ be the $n \times n$ identity matrix and define the standard complex structure

$$J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix},$$

which satisfies $J^2 = -1$. In the Lean development this matrix is PassivityUn.stdJ n, and the index type is PassivityUn.Blk n, the disjoint union of two copies of Fin n.

Two real linear subspaces of the $4n^2$-dimensional space of such matrices are defined:

1. symm n: the symmetric matrices, $W^{\mathsf T} = W$;
2. commJ n: the matrices commuting with $J$, $WJ = JW$.

The admissible coupling class admissible n is their intersection:

$$\mathcal{A}_n = \{\, W \in \mathbb{R}^{2n \times 2n} : W^{\mathsf T} = W \ \text{and}\ WJ = JW \,\}.$$

Formalization targets

Goal: the admissible class has dimension $n^2$

$$\dim_{\mathbb{R}} \mathcal{A}_n = n^2 \qquad \text{for every } n \in \mathbb{N}.$$

This is PassivityUn.admissible_finrank. It asserts the exact dimension for all $n$ at once, not for a particular node size.

Milestones

1. M1. $J \cdot J = -1$, so $J$ is a complex structure.
2. M2. A block matrix $\begin{pmatrix} A & B \\ C & D \end{pmatrix}$ commutes with $J$ exactly when $D = A$ and $B = -C$.
3. M3. A block matrix $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$ is symmetric exactly when $A^{\mathsf T} = A$ and $B^{\mathsf T} = -B$.
4. M4. The dimension counts of symmetric and antisymmetric $n \times n$ matrices add to $n^2$: $\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$.

Significance

The result itself. The goal identifies the admissible coupling class with the real form of the $n \times n$ Hermitian matrices, the space whose dimension is that of $\mathfrak{u}(n)$ (Hermitian matrix). Applied at $n = 1, 2, 3$ it gives the dimensions $1$, $4$ and $9$, which the Shape Zero model matches with $\mathfrak{u}(1)$, $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$. Without a proof for general $n$, the model rests on a finite numerical check.

Formalizing it. The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps (Linear complex structure). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general-$n$ statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise.

Difficulty

Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the $2n \times 2n$ matrix indexed by a disjoint union and its four $n \times n$ blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every $n$.

Formalization scope

• Matrices are real (ℝ), not complex. The complex structure enters only through the fixed real matrix $J$.
• Matrices are indexed by Fin n ⊕ Fin n (PassivityUn.Blk n) rather than Fin (2n), so that block decomposition via Mathlib's Matrix.fromBlocks is direct. The first copy of Fin n indexes the upper/left blocks.
• Each condition is defined as the kernel of a linear map: symmetry as the kernel of $W \mapsto W^{\mathsf T} - W$, and commuting with $J$ as the kernel of $W \mapsto WJ - JW$. Both are therefore subspaces by construction, with no hand-written closure proofs.
• Dimension is Module.finrank ℝ. The ambient space is finite-dimensional, so the convention that finrank of an infinite-dimensional space is $0$ never applies.
• The case $n = 0$ is included, and there the statement reads $0 = 0$. This is not a trivialization: the claim is quantified over all $n$, and every $n \ge 1$ is a nontrivial instance.
• M4 is stated with natural-number division and truncated subtraction. Both are exact here, because $n(n \pm 1)$ is always even and $n \cdot (n - 1) = 0$ when $n = 0$.

The development needs only Mathlib's block matrices, transpose, linear maps and finrank. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with $J$ to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism.

Selected references

• B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
• Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
• Wikipedia, Linear complex structure. https://en.wikipedia.org/wiki/Linear_complex_structure
• Wikipedia, Hermitian matrix. https://en.wikipedia.org/wiki/Hermitian_matrix
• Mathlib, Mathlib.Data.Matrix.Block (block matrices, Matrix.fromBlocks). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.html

Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.

Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.

Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.

Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.

Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.

Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.

Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.

Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.

Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.

The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.

Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.

Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.

The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.

Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Why initialization matters for transfer learning

Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.

LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.

Linear predictors, training data, and OOD loss

An input is a vector $x\in\mathbb R^d$. A feature extractor is a matrix $B\in\mathbb R^{k\times d}$, and a head is a vector $v\in\mathbb R^k$. Together they predict $v^\top Bx$, with effective weight vector $B^\top v$. The fixed matrix $X\in\mathbb R^{n\times d}$ contains the $n$ training inputs as rows. Their span is $S=\operatorname{rowspace}(X)$, with dimension $m$.

The ground truth has orthonormal-row features $B_\star$ and a nonzero head $v_\star$. Write $w_\star=B_\star^\top v_\star$ and $Y=Xw_\star$. Perfect pretrained features mean $B_0=UB_\star$ for an orthogonal matrix $U$. The corresponding aligned head is $u=Uv_\star$. The dimensions satisfy $1\le k\le m$ and $m+k<d$.

The two geometric assumptions require the orthogonal projections from $R_0=\operatorname{rowspace}(B_0)$ into $S$ and into $S^\perp$ to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of $v\mapsto\Pi_T B_0^\top v$ for each $T\in\{S,S^\perp\}$. See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.

An out-of-distribution law $\mu$ is any probability measure on $\mathbb R^d$ with a finite second moment and positive-definite uncentered second-moment matrix $\Sigma=\mathbb E_\mu[xx^\top]$. Its mean need not be zero. Define

$$L_{\rm OOD}(v,B)=\mathbb E_{x\sim\mu} [(v^\top Bx-w_\star^\top x)^2].$$

Both training methods use the unnormalized loss $\widehat L(v,B)=\|XB^\top v-Y\|_2^2$. Fine-tuning follows its gradient flow in both parameters; linear probing keeps $B=B_0$. Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.

Formalization targets

The goal is Proposition 3.7 in an explicit nonzero-signal regime. For $\sigma>0$, initialize an FT head with independent Gaussian coordinates, $v_0\sim\mathcal N(0,\sigma^2I_k)$. Establish

$$\Pr\!\left[\forall t\ge0,\quad L_{\rm OOD}(v_{\rm FT}(t),B_{\rm FT}(t))>0\right]=1.$$

Linear probing, from any initial head, must converge to $u$. Fine-tuning initialized at its limit must satisfy

$$v_{\rm LP}(t)\longrightarrow u,\qquad \forall t\ge0,\quad L_{\rm OOD}(v_{\rm LP\text{-}FT}(t),B_{\rm LP\text{-}FT}(t))=0.$$

The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.

Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.

What the result establishes

The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.

The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.

Why the proof needs the training dynamics

The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.

Formalization scope and conventions

Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within $[0,\infty)$, including the right derivative at zero.

The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; $k\le m$ makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.

The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.

Selected references

• Ananya Kumar, Aditi Raghunathan, Robbie Jones, Tengyu Ma, and Percy Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, arXiv:2202.10054v1. Main target: Section 3.4, Proposition 3.7, PDF p. 10, equations (3.10)-(3.11); proof: Appendix A.7, PDF pp. 45-47, Proposition A.20 and (A.208)-(A.218). Supporting invariants: Appendix A.2, PDF p. 24, Lemmas A.3-A.4, equations (A.15)-(A.20). Gaussian alignment: Appendix A.3, PDF pp. 34-35, Lemmas A.11-A.12.