Optimization

Motivation

Least squares fits a linear model $Ax \simeq b$ by minimizing $\|Ax - b\|$, and its solution can be extremely sensitive to errors in the data $(A, b)$ when $A$ is ill-conditioned. The standard remedy is Tikhonov regularization (ridge regression): minimize $\|Ax - b\|^2 + \mu\|x\|^2$, whose solution $x = (A^\top A + \mu I)^{-1}A^\top b$ is stable but depends on a parameter $\mu > 0$ that must be chosen by some external rule.

El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed instead to take the uncertainty in $(A, b)$ seriously: the robust least-squares (RLS) solution minimizes the worst-case residual over all perturbations $[\Delta A\ \Delta b]$ of Frobenius norm at most $\rho$. Their Theorem 3.1 shows that for $\rho = 1$ this worst-case residual equals $\|Ax - b\| + \sqrt{\|x\|^2 + 1}$ and that its minimization is the second-order cone program (15). Theorem 3.2, the subject of this mission, reads off the optimal solution: it is a Tikhonov-regularized solution, and the regularization parameter is not a free choice but is fixed by the data. This gives a principled answer to the question of how to choose $\mu$, and it is the reason the paper describes RLS as "a Tikhonov regularization procedure" with "a rigorous way to compute the regularization parameter" (abstract, p. 1035).

A closely related model for least squares with bounded data uncertainty was developed at the same time by Chandrasekaran, Golub, Gu and Sayed; the paper notes that their preliminary draft (its reference [5]) gives a solution to the unstructured RLS problem similar to that of §3.2 (pp. 1036–1037).

Setting

Throughout, $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^n$, $x \in \mathbb R^m$, and every vector norm is Euclidean, $\|v\| = \sqrt{\sum_i v_i^2}$. For $x \in \mathbb R^m$, $[x; 1] \in \mathbb R^{m+1}$ is $x$ with a coordinate $1$ appended, so $\|[x;1]\| = \sqrt{\|x\|^2 + 1}$.

The SOCP (15) is the problem, in the variables $x \in \mathbb R^m$ and $\lambda, \tau \in \mathbb R$,

A triple $(x, \lambda, \tau)$ is optimal for (15) if it is feasible and $\lambda \le \lambda'$ for every feasible $(x', \lambda', \tau')$. Its dual, derived in the paper from the general second-order cone duality of §2.1, is the problem in $z \in \mathbb R^n$, $u \in \mathbb R^m$, $v \in \mathbb R$

The minimum-norm solution of $Ax = b$ is a solution $x$ with $\|x\| \le \|y\|$ for every other solution $y$; when $Ax = b$ is consistent it is $A^\dagger b$, with $A^\dagger$ the Moore–Penrose pseudoinverse.

In the Lean development these objects are IsSOCPFeasible, IsSOCPOptimal, IsDualFeasible, dualObjective, IsDualOptimal and IsMinNormSolution, in the namespace RobustLS.Tikhonov, with the Euclidean norm eucNorm.

Formalization targets

Goal: Theorem 3.2 with the identity for $\mu$

Let $(x, \lambda, \tau)$ be optimal for (15) and set $\mu = (\lambda - \tau)/\tau$. Then

By Theorem 3.1 (the subject of the companion mission I of this series), the $x$-part of an optimal point of (15) is the RLS solution for $\rho = 1$, so this is formula (17) of the paper. The identity for $\mu$ is the final display of the paper's proof and is the claim in the mission's title.

Milestones (in the order of the paper's proof, p. 1041)

1. Both (15) and its dual have optimal points.
2. If $\lambda = \tau$ at the optimum, then $Ax = b$ and $\lambda = \tau = \sqrt{\|x\|^2 + 1}$.
3. In that case $x$ is the minimum-norm solution of $Ax = b$, $x = A^\dagger b$.
4. Eq. (18): for $\lambda > \tau$, primal and dual optimal values coincide,

5. The dual optimal point is $z = -(Ax - b)/\|Ax - b\|$, $[u; v] = -[x; 1]/\sqrt{\|x\|^2 + 1}$.
6. Substituting into $A^\top z + u = 0$: $x = (A^\top A + \mu I)^{-1}A^\top b$ with $\mu = (\lambda - \tau)/\tau = \|Ax - b\|/\sqrt{\|x\|^2 + 1}$.

A further item states Remark 3.1: for $\lambda > \tau$, $x$ is the unique minimizer of the weighted residual $\big\|[A; I; 0]y - [b; 0; 1]\big\|_\Theta$ with $\Theta = \mathbf{diag}((\lambda-\tau)I, \tau I, \tau)$ and $\|r\|_\Theta = \|\Theta^{-1/2} r\|$.

Significance

The result. Theorem 3.2 turns a robust optimization problem into a familiar linear-algebra object. It says that the robust solution always lies on the Tikhonov path $\{(A^\top A + \mu I)^{-1}A^\top b : \mu > 0\}$ or at its endpoint $A^\dagger b$, and it identifies the point on the path through a fixed-point equation relating $\mu$ to the residual and the size of the solution. The paper builds on this in §3.3 (a one-dimensional search for $\mu$ via the SVD) and in §6 (continuity of the RLS solution in the data), and Remark 3.1 is the template for the weighted least-squares interpretation of the structured and linear-fractional problems in §5.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of second-order cone duality for a concrete program, the characterization of the optimal dual point by equality in the Cauchy–Schwarz inequality, and the minimum-norm characterization of $A^\dagger b$, all in terms of explicit Euclidean norms on Fin k → ℝ.

Difficulty

The paper's proof rests on strong duality for (15) ("both primal and dual problems are strictly feasible"), which it cites from the SOCP literature rather than proving; Mathlib has no second-order cone duality, so this step is the main gap. The degenerate case $\lambda = \tau$ also needs care: there $\|Ax - b\| = 0$, the residual term is not differentiable at the optimum, and the conclusion changes from a regularized inverse to a pseudoinverse. A statement that only handles the case $Ax \ne b$, or that assumes the matrix $A^\top A + \mu I$ invertible without deriving it from $\mu > 0$, misses part of the theorem.

Formalization scope

• Normalization. The paper states Theorem 3.2 for $\rho = 1$ ("we take $\rho = 1$ in what follows", p. 1039) and obtains general $\rho$ by the scaling $\varphi(A, b, \rho) = \rho\,\varphi(A/\rho, b/\rho, 1)$. Only the $\rho = 1$ statement is formalized.
• The RLS solution. The perturbation model is not used here: all statements are about optimal points of (15). That the $x$-part of such a point is the RLS solution is Theorem 3.1 (mission I), and it is recalled in prose only.
• Norms. Vectors are Fin k → ℝ; the Euclidean norm is the explicit eucNorm v = √(∑ vᵢ²) (Mathlib's ‖·‖ on Fin k → ℝ is the sup norm). Stacked vectors $[x;1]$ and $[u;v]$ are indexed by Fin m ⊕ Unit.
• Optimality. "Optimal point" means feasible with objective no worse than every feasible point; the minimum and maximum are therefore attained by definition, and milestone 1 guarantees they exist.
• Pseudoinverse. Mathlib has no matrix pseudoinverse, so $A^\dagger b$ is stated as the minimum-norm solution of $Ax = b$, which is how the proof uses it. The branch "else" is $\neg(\mu > 0)$.
• Inverse. $(\mu I + A^\top A)^{-1}$ is Mathlib's Matrix.inv; it is used only where $\mu > 0$, where the matrix is positive definite. $\tau \ge 1$ at every feasible point, so $\mu$ is well defined without an extra hypothesis.
• No trivialization. The goal quantifies over optimal points of (15) over the whole feasible set, not over feasible points, and milestone 1 shows the hypothesis is satisfiable for every $(A, b)$, including $n = 0$ or $m = 0$.
• Weighted norm. For Remark 3.1, $\|r\|_\Theta$ for the diagonal $\Theta$ is written as $\sqrt{\sum_i r_i^2/\theta_i}$, which equals $\|\Theta^{-1/2}r\|$ for positive weights.

Contributions welcome: second-order cone (or general conic) weak and strong duality for finite-dimensional programs, the equality case of Cauchy–Schwarz in the explicit-norm form used here, and a Moore–Penrose pseudoinverse for real matrices with its minimum-norm property. The platform's ConvexOptimization.conic_slater_strong_duality may help with the duality step.

Selected references

• L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• S. Chandrasekaran, G. H. Golub, M. Gu and A. H. Sayed, A new linear least-squares type model for parameter estimation in the presence of data uncertainties, cited as submitted to SIAM J. Matrix Anal. Appl. (reference [5] of the paper).
• A. N. Tikhonov and V. Y. Arsenin, Solutions of Ill-Posed Problems, Wiley, New York, 1977 (reference [43] of the paper).
• Y. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra Appl. 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

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

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

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

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

Milestones

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

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

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

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

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:

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$

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

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):

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

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$,

The proximal problem (2.8) is

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))$.