Convex Optimization

Motivation

Training a model in machine learning means minimizing an expected loss over a data distribution, using a finite sample from it. Two families of methods dominate. Stochastic gradient methods step along the gradient of the loss at one data point: each step is cheap, but the noise forces small steps and many sequential iterations. Batch methods average the gradient over a large set of points: each step is accurate and parallelizes well, but costs a pass over the data. Bottou and Bousquet (The tradeoffs of large scale learning, NIPS 2007) compared the two by the total work needed to reach accuracy $\epsilon$ and concluded that stochastic gradient descent is preferable in large-scale learning.

Byrd, Chin, Nocedal and Wu (Sample size selection in optimization methods for machine learning, Math. Program. 2012) analyse a third option: a dynamic batch method, which takes gradient steps on mini-batches whose size grows over the run. A small batch makes early progress cheap; a large batch later makes the steps accurate. Their Theorem 4.2 shows that when the batch size grows geometrically, steepest descent with a fixed step converges linearly in expectation, and their Corollary 4.3 derives from it a total work bound of the same order as stochastic gradient descent. The analysis underlies a line of work on adaptive sampling and variance-controlled batch methods (for example Friedlander and Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 2012; Bottou, Curtis and Nocedal, Optimization methods for large-scale machine learning, SIAM Review 2018, §5.2).

Setting

Let $(Z,P)$ be a probability space of data points $z$; in the paper $z=(x,y)$ is an input–output pair with distribution $P(x,y)$. The parameter is $w\in\mathbb R^m$ ($m$ is the number of variables). A per-sample loss $\ell(w;z)$ is given with gradient $\nabla\ell(w;z)$ in $w$, and the objective is the expected loss (2.1)

$$J(w)=\int\ell(w;z)\,dP(z).$$

The gradient of the objective is the expected per-sample gradient, $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$.

Uniform convexity (4.2): $J$ is twice continuously differentiable and there are constants $0<\lambda<L$ with

$$\lambda\|d\|_2^2\le d^T\nabla^2J(w)\,d\le L\|d\|_2^2\qquad\text{for all } w,d .$$

Then $J$ has a unique minimizer $w^*$.

For a random vector $X\in\mathbb R^m$, $\|\mathrm{Var}(X)\|_1=\mathbb E\|X-\mathbb EX\|_2^2$ is the sum of its componentwise variances. The variance bound (4.22) asks for a constant $\omega$ with

$$\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1\le\omega\qquad\text{for all } w .$$

The algorithm. Fix sample sizes $n_k\ge1$ and a starting point $w_0$. At iteration $k$ draw a batch $S_k$ of $n_k$ points, independently with law $P$ and independently of earlier batches, form the batch gradient (4.19)

$$g_k=\frac1{n_k}\sum_{i\in S_k}\nabla\ell(w_k;i),$$

and take the dynamic batch steepest descent step (4.24)

$$w_{k+1}=w_k-\frac1L\,g_k .$$

The iterates $w_k$ are random, and expectations below are over all batches.

Formalization targets

Goal: Theorem 4.2

If $n_k\ge a^k$ for all $k$, for some $a>1$, and (4.22) holds, then

$$\mathbb E[J(w_k)-J(w^*)]\le C\rho^k\quad\text{for all }k,\qquad \rho=\max\{1-\lambda/(4L),\,1/a\}<1,\quad C=\max\{J(w_0)-J(w^*),\,2\omega/\lambda\}.$$

The constants are the paper's. The goal also asserts that $J(w_k)$ is integrable for every $k$.

Milestones, in the order the proof uses them

1. (4.5), p. 8: $\nabla J(w)^T\nabla J(w)\ge\lambda[J(w)-J(w^*)]$ for every $w$.
2. Taylor bound, p. 11: $J(w-\frac1Lg)\le J(w)-\frac1L\nabla J(w)^Tg+\frac1{2L}\|g\|^2$ for every $w$ and $g$.
3. (4.25), p. 11: at a fixed point $w$, with $g$ the batch gradient of $n$ i.i.d. draws,

$$\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1L\|\nabla J(w)\|^2+\tfrac1{2L}\mathbb E\|g\|^2,\qquad \mathbb E\|g\|^2=\|\nabla J(w)\|^2+\|\mathrm{Var}(g)\|_1 .$$

4. Variance of the batch gradient, p. 12: $\|\mathrm{Var}(g)\|_1\le\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1/n$.
5. (4.26), p. 12: $\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1{2L}\|\nabla J(w)\|^2+\tfrac1{2Ln}\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1$.
6. (4.27), p. 12: $\mathbb E[J(w-\tfrac1Lg)-J(w^*)]\le(1-\tfrac{\lambda}{2L})(J(w)-J(w^*))+\tfrac{\omega}{2Ln}$.

Milestones 3–6 are the paper's conditional expectations given $w_k$, stated at a fixed point $w$ with the batch drawn afresh.

Significance

Theorem 4.2 is the convergence guarantee of the dynamic sampling strategy: it says that the noise of a mini-batch gradient does not destroy the linear rate of steepest descent, provided the batch grows geometrically. The rate $\rho$ makes the trade-off explicit: the optimization contracts by $1-\lambda/(4L)$ per step, the noise by $1/a$, and the slower of the two governs. From it the paper's Corollary 4.3 bounds the total number of sample-gradient evaluations to reach $\mathbb E[J(w_k)-J(w^*)]\le\epsilon$ by $O(L/(\lambda\epsilon))$, which places dynamic batch methods on the same footing as stochastic gradient descent in the Bottou–Bousquet comparison, while keeping the parallelism of batch methods.

The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization produces a reusable account of the one-iteration analysis of a mini-batch gradient step (descent lemma, variance of an i.i.d. sample mean of random vectors, conditional expectation over a fresh batch), and of the passage from a conditional one-step recursion to an unconditional bound over a run driven by an infinite i.i.d. array. Corollary 4.3 is not part of this mission: it involves $O(\cdot)$ bounds, a cost model for gradient evaluations and an iteration count treated as a real number.

Difficulty

The arithmetic of the induction on p. 12 is short. The difficulty is in making the probability rigorous. The iterate $w_k$ is random, and the paper's one-step bound (4.27) is a conditional expectation given $w_k$, with $J(w_k)$ on the right-hand side. Turning it into an unconditional recursion requires that the batch of iteration $k$ be independent of $w_k$, that $w_k$ be a measurable function of the earlier batches, and that $J(w_k)$ and $\|g_k\|^2$ be integrable at every step, none of which is automatic for a run driven by an infinite array of draws. A naive formalization that treats $w_k$ as a fixed point, or $g_k$ as an abstract random vector with a postulated variance bound, skips exactly this content.

The variance identity for a sample mean of random vectors in $\mathbb R^m$ and the bound $\|\nabla J(w)\|\le L\|w-w^*\|$ from (4.2) are standard but not packaged in this form in Mathlib.

Formalization scope

• The space is EuclideanSpace ℝ (Fin m). The paper's $\lambda$ is written lam (λ is a Lean keyword). (4.2) is ContDiff ℝ 2 J, 0 < lam < L, and the two-sided bound on fderiv ℝ (fderiv ℝ J) w d d.
• $J$ is defined as the Bochner integral $\int\ell(w;z)\,dP(z)$ for a general per-sample loss $\ell$; the paper's linear predictor $f(w;x)=w^Tx$ and convex loss $l$ are not used by the theorem and are not assumed. The model assumes: $\ell(w;\cdot)$ integrable; $\nabla\ell(w;z)$ the gradient of $\ell(\cdot;z)$ at $w$; $(w,z)\mapsto\nabla\ell(w;z)$ jointly measurable; $\nabla\ell(w;\cdot)$ square-integrable; and $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$ (differentiation under the integral, which the paper uses without proof).
• Sampling with replacement. The paper's (3.5) is sampling without replacement from $N$ points; it takes $N\to\infty$ on p. 5, which "also corresponds to the case of sampling with replacement". The formalization draws every point i.i.d. from $P$: draw $i$ of iteration $k$ is $\xi_{k,i}$ and the law of the whole array is Measure.infinitePi over $\mathbb N\times\mathbb N$. The finite-population factor $(N-n_k)/(N-1)$ is not modelled.
• $w^*$ is a given minimizer of $J$; $n_k$ are natural numbers with $a^k\le n_k$ (real powers of a real $a>1$); $\omega$ is a real number.
• The goal asserts integrability of $J(w_k)$ together with the bound, so the inequality cannot be met by the Bochner integral's value $0$ on a non-integrable function. The batch gradient is the mean over $n_k$ draws at the current iterate, and $w_k$ is the random run: a goal with an abstract random $g_k$ satisfying a postulated variance bound, or with $w_k$ a deterministic sequence, would not be this theorem.
• Welcome contributions: the variance of an i.i.d. mean of $\mathbb R^m$-valued random vectors; the descent lemma and gradient-dominance inequality from Hessian bounds; measurability and independence lemmas for processes driven by Measure.infinitePi. All three are reusable beyond this mission.

Selected references

• R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012) 127–155. https://doi.org/10.1007/s10107-012-0572-5
• L. Bottou, O. Bousquet, The tradeoffs of large scale learning, NIPS 2007. https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning
• M. P. Friedlander, M. Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 34 (2012) A1380–A1405. https://doi.org/10.1137/110830629
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization methods for large-scale machine learning, SIAM Review 60 (2018) 223–311. https://doi.org/10.1137/16M1080173

Motivation

Training a machine-learning model usually means minimizing an expected or empirical loss $J(w)$ over parameters $w \in \mathbb{R}^m$. Exact gradients of such objectives are expensive, because each one requires a pass over the whole data set; practical methods replace $\nabla J(w_k)$ by a cheaper approximation $g_k$, for instance a gradient computed on a subsample. This raises a basic question for the analysis of optimization algorithms: how accurate must the approximate gradient be for steepest descent to keep its linear rate of convergence?

Byrd, Chin, Nocedal and Wu (Math. Program. 2012) answer this question with a relative-error condition, and use the answer to motivate a rule that increases the sample size during the run. Their §4.1 treats the deterministic case: the approximations $g_k$ are arbitrary vectors, and only a geometric condition linking $g_k$ to $\nabla J(w_k)$ is assumed. That deterministic result, Theorem 4.1, is the goal of this mission. The stochastic counterpart (Theorem 4.2, dynamic batch sizes) is a separate mission of the same series.

Relative-error conditions of this kind ("the error is a fixed fraction of the step") appear throughout the literature on inexact gradient and inexact Newton methods (e.g. Bertsekas and Tsitsiklis 2000 on gradient methods with errors), and the condition (4.8) below is the deterministic template for the adaptive sampling tests later developed for stochastic optimization.

Setting

Let $J : \mathbb{R}^m \to \mathbb{R}$ be twice continuously differentiable and uniformly convex: there are constants $0 < \lambda < L$ such that

$$\lambda\|d\|_2^2 \;\le\; d^T \nabla^2 J(w)\, d \;\le\; L\|d\|_2^2 \qquad\text{for all } w, d \in \mathbb{R}^m. \tag{4.2}$$

Such a $J$ has a unique minimizer $w_*$; following the paper, it is normalized so that $J(w_*) = 0$.

Fix $\theta \in (0,1)$. Given a sequence of vectors $g_0, g_1, \ldots$ (the approximate gradients), the fixed-steplength steepest descent iteration is

$$w_{k+1} = w_k - \alpha g_k, \qquad \alpha = \frac{1-\theta}{L}. \tag{4.1, 4.7}$$

The approximate gradient at iteration $k$ satisfies the relative-error condition if

$$\|g_k - \nabla J(w_k)\| \;\le\; \theta\, \|g_k\|. \tag{4.8}$$

Write

$$\beta = \frac{(1-\theta)^2}{2(1+\theta)^2}. \tag{4.9}$$

Formalization targets

Goal: Theorem 4.1 (p. 8)

1. If (4.8) holds at iteration $k$, then

$$J(w_{k+1}) \le \Bigl(1 - \frac{\beta\lambda}{L}\Bigr) J(w_k). \tag{4.9}$$

2. If (4.8) holds at every iteration, then $w_k \to w_*$ (4.10); every $k > \frac{L}{\beta\lambda}[\log(1/\epsilon) + \log J(w_0)]$ satisfies $J(w_k) < J(w_*) + \epsilon$ (4.11); and

$$\|g_k\|^2 \le \frac{1}{(1-\theta)^2}\,\frac{2L^2J(w_0)}{\lambda}\Bigl(1-\frac{\beta\lambda}{L}\Bigr)^k. \tag{4.12}$$

The constants are those of the paper and are kept explicit.

Milestones

In the order the paper's proof uses them:

• (4.5) $\nabla J(w)^T\nabla J(w) \ge \lambda[J(w) - J(w_*)]$ and (4.6) $J(w) - J(w_*) \ge \frac{\lambda}{2L^2}\|\nabla J(w)\|_2^2$, consequences of (4.2) alone (p. 8);
• (4.13) $(1-\theta)\|g_k\| \le \|\nabla J(w_k)\| \le (1+\theta)\|g_k\|$ and (4.14) $\nabla J(w_k)^Tg_k \ge (1-\theta)\|g_k\|^2$ under (4.8) (p. 9);
• (4.16) the one-step decrease $J(w_{k+1}) \le J(w_k) - \frac{\beta}{L}\|\nabla J(w_k)\|^2$ under (4.8) at $k$ (p. 9);
• (4.17) $J(w_k) \le (1 - \beta\lambda/L)^k J(w_0)$ under (4.8) at every earlier iteration (p. 9).

Significance

Theorem 4.1 says that the linear convergence of steepest descent on a uniformly convex function survives arbitrary gradient errors, provided each error is at most a fixed fraction $\theta$ of the approximate gradient's own norm. The price is explicit: the per-step contraction factor is $1 - \beta(\theta)\lambda/L$ instead of a factor of the form $1 - c\lambda/L$ with an absolute constant $c$, and the iteration bound (4.11) grows like $L/(\beta\lambda)$ times a logarithm. Because (4.8) is relative rather than absolute, no a priori bound on the error is needed, and the error may be large far from the solution. In the paper this is the motivation for requiring the sample variance of a subsampled gradient to be small relative to $\|g_k\|^2$, which leads to the dynamic sample-size rule analysed in §4.2.

The result is proved in the paper (pp. 9–10). No machine-checked proof of it, or of any relative-error inexact gradient method with explicit constants, has been published. A formal proof provides a checked reference statement for inexact first-order methods with the paper's constants, and the milestones (4.5), (4.6), (4.13), (4.14) are reusable facts about strongly convex smooth functions and about relative-error gradient approximations.

Difficulty

Each step is classical, but the proof combines second-order information with metric estimates. The descent estimate (4.15) needs a second-order Taylor bound from the upper Hessian bound in (4.2), which in Lean means passing from a bound on the second Fréchet derivative to a quadratic upper bound on $J$ along a segment. The inequalities (4.5) and (4.6) relate the gradient norm to the optimality gap through the lower and upper Hessian bounds and the minimizer, and must be derived without an explicit averaged Hessian unless one is built. The convergence $w_k \to w_*$ in (4.10) requires turning convergence of the function values into convergence of the iterates, which again uses uniform convexity. Finally, (4.11) is a logarithmic iteration count whose boundary cases ($J(w_0) = 0$, $\epsilon \ge J(w_0)$) must be handled. A naive reading of the iteration with exact gradients does not apply: the step is $(1-\theta)/L$, not $1/L$, and the direction $-g_k$ is only known to be a descent direction through (4.14).

Formalization scope

The space is EuclideanSpace ℝ (Fin m). Assumption (4.2) is a definition HessianBounds J lam L (with lam for $\lambda$, a Lean keyword): ContDiff ℝ 2 J, 0 < lam < L, and both bounds on the quadratic form fderiv ℝ (fderiv ℝ J) w d d. The gradient is Mathlib's gradient J. The minimizer is a point wstar with J wstar ≤ J w for all w, and J wstar = 0 is a hypothesis of the goal and of (4.17), exactly as in the paper; (4.5) and (4.6) are stated with $J(w_*)$ and without it. The constant $\beta$ is a definition beta θ; it is never a free variable. The approximate gradients $g_k$ are an arbitrary sequence and nothing is random. The iterates are any sequence with w (k+1) = w k - ((1 - θ) / L) • g k for all k.

The one-step claim (4.9) assumes (4.8) only at the index $k$; (4.10)–(4.12) assume it at every index. (4.11) is stated in the form the proof derives in (4.18): every $k$ strictly beyond the bound has $J(w_k) < \epsilon$. The logarithm is natural; when $J(w_0) = 0$ Lean's convention $\log 0 = 0$ applies, which is harmless because every iterate is then optimal. No positivity hypothesis on $J(w_0)$ is added.

A trivializing formalization is excluded: the step size is fixed by the paper, $\beta$ and the Hessian bounds are pinned, and the hypotheses are satisfiable, e.g. by $J(w) = \tfrac{c}{2}\|w\|^2$ with $\lambda < c < L$, $w_* = 0$ and $g_k = \nabla J(w_k)$.

A complete development needs: a second-order Taylor (or mean-value) bound from a Hessian bound, the strong-convexity inequalities (4.5)–(4.6), and elementary real-analysis facts about geometric sequences and logarithms. The milestones (4.5), (4.6), (4.13) and (4.14) are independent of the iteration and reusable. Proofs of any milestone, and alternative proofs with sharper constants stated as separate theorems, are welcome.

Selected references

• R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012), 127–155. https://doi.org/10.1007/s10107-012-0572-5
• D. P. Bertsekas, J. N. Tsitsiklis, Gradient convergence in gradient methods with errors, SIAM Journal on Optimization 10 (2000), 627–642. https://doi.org/10.1137/S1052623497331063
• L. Bottou, O. Bousquet, The tradeoffs of large scale learning, Advances in Neural Information Processing Systems 20 (2008). https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning

Motivation

Semidefinite representations may be smaller than linear descriptions of a polytope. Lower bounds for their matrix size require a factorization obstruction that applies to arbitrary positive-semidefinite factors. The source manuscript presents the surrounding research claim.

Setting

For even n, columns are perfect matchings of the complete graph. Rows comprise edges and odd vertex subsets. The unshifted slack matrix has edge-incidence entries and odd-cut entries |M∩δ(U)|−1. Its real PSD rank is the least positive r admitting trace products of positive-semidefinite r×r factors.

Formalization target

Prove that every positive real power is eventually exceeded:

$$\forall C>0\;\exists n_0\ge4\;\forall\text{ even }n\ge n_0,\qquad n^C<\operatorname{psdRank}(n).$$

The separate lift target gives the same superpolynomial lower bound for every exact affine PSD lift.

The selected formal target is OAI.PerfectMatchingPSD.main.

Significance and status

The selected formal goal excludes polynomial-size factorizations. The manuscript dated October 5 states exponential bounds for positively shifted matching matrices; that stronger shifted statement is not the existing published target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Factors are unrestricted real PSD matrices, with no rank-one or symmetry requirement. Lower bounds for nonnegative rank alone do not rule them out.

Formalization scope

The target concerns the full unshifted row set and uses real exponentiation with C fixed before n₀. The affine-lift companion quantifies over affine sections and affine images of PSD cones. Independent definition groups are retained separately. The description deliberately makes no exponential or positive-shift claim for these references.

Selected references

• OpenAI, Exponential PSD rank of positively shifted matching matrices, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem $\min \operatorname{rank}(X)$ subject to $\mathcal S(X) = \mathcal M$ is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization $\min \|X\|_*$ subject to $\mathcal S(X) = \mathcal M$ or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).

Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that $\mathcal S$ nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of $\mathcal S$ be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.

Timeline.

• 2005: Candès and Tao introduce restricted isometry constants for sparse vectors and prove exact recovery by $\ell_1$ minimization under a condition on them (IEEE Trans. Inf. Theory).
• 2008: Candès shows that $\delta_{2s} < \sqrt 2 - 1$ suffices in the vector case (C. R. Math.).
• 2010: Recht, Fazel and Parrilo define the rank restricted isometry property and prove that nuclear-norm minimization recovers every rank-$r$ matrix when $\delta_{5r}$ is small enough (SIAM Review).
• 2011: Candès and Plan prove the matrix analogue of the $\sqrt 2 - 1$ threshold and the orthogonality estimate quoted here as Lemma 6.9 (IEEE Trans. Inf. Theory).
• 2011: Fornasier, Rauhut and Ward prove Proposition 6.8, the target of this mission: $\delta_{4k} < \sqrt 2 - 1$ implies the SRNSP of order $k$.

Setting

Fix integers $n, p, m$. A measurement map is a linear map $\mathcal S : \mathbb R^{n\times p} \to \mathbb R^m$; it is given by $m$ matrices $A_1,\dots,A_m$ through $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$, where $\langle X, Y\rangle = \operatorname{Tr}(XY^{\top}) = \sum_{i,j} X_{ij}Y_{ij}$. The Frobenius norm is $\|X\|_F = \langle X, X\rangle^{1/2}$, the nuclear norm $\|X\|_*$ is the sum of the singular values of $X$, and $\|\mathcal S(X)\|_{\ell_2^m}$ is the Euclidean norm of the vector $\mathcal S(X)$. A matrix is $k$-rank if its rank is at most $k$.

The restricted isometry constant $\delta_k = \delta_k(\mathcal S)$ (Definition 1.1) is the smallest $\delta \ge 0$ such that

$$(1 - \delta)\|X\|_F^2 \le \|\mathcal S(X)\|_{\ell_2^m}^2 \le (1+\delta)\|X\|_F^2 \qquad \text{for all $k$-rank } X .$$

The map $\mathcal S$ has the strong rank null space property of order $k$ with constant $\eta \in (0,1)$ (Definition 6.4) if for every $X \in \ker \mathcal S \setminus\{0\}$ and every decomposition $X = X_1 + X_2$ with $X_1$ $k$-rank, there is another decomposition $X = H_1 + H_2$ with $\operatorname{rank} H_1 \le 2k$, $\langle H_1, H_2\rangle = 0$, $X_1H_2^{\top} = 0$, $X_1^{\top}H_2 = 0$, and

$$\|H_1\|_* \le \eta\,\|H_2\|_* .$$

In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X $= \|\mathcal S(X)\|^2_{\ell_2^m}$, built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).

Formalization targets

Goal: Proposition 6.8

If $\delta_{4k} > 0$ and

$$\delta_{4k} < \sqrt 2 - 1,$$

then $\mathcal S$ satisfies the SRNSP of order $k$ with constant

$$\eta = \sqrt 2\,\frac{\delta_{4k}}{1 - \delta_{3k}} \in (0,1).$$

The constant $\eta$ is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including $\eta \in (0,1)$.

Milestones

1. Lemma 6.9 (Candès–Plan): for $\langle X, Y\rangle = 0$ and $\operatorname{rank}X + \operatorname{rank}Y \le k$, $|\langle \mathcal S(X), \mathcal S(Y)\rangle| \le \delta_k \|X\|_F\|Y\|_F$.
2. Lemma 6.10 (Recht–Fazel–Parrilo): $XZ^{\top} = 0$ and $X^{\top}Z = 0$ imply $\|X + Z\|_* = \|X\|_* + \|Z\|_*$.
3. The block decomposition of the proof: relative to an SVD $X_1 = U(\begin{smallmatrix}\Sigma & 0\\ 0 & 0\end{smallmatrix})V^{\top}$, the matrices $H_0$ and $H_c$ obtained by zeroing blocks of $U^{\top}XV$ satisfy $X = H_0 + H_c$, $\operatorname{rank}H_0 \le 2k$, $X_1H_c^{\top} = 0$, $X_1^{\top}H_c = 0$, $\langle H_0, H_c\rangle = 0$.
4. $\|H\|_* \le \sqrt r\,\|H\|_F$ for $\operatorname{rank}H \le r$, and $\|H\|_F \le \|H + K\|_F$ for $\langle H, K\rangle = 0$.
5. The shelling bound: for a nonincreasing nonnegative sequence cut into blocks of length $\ell$, each block's $\ell_2$ norm is at most $\ell^{-1/2}$ times the $\ell_1$ norm of the previous block.
6. Monotonicity $\delta_k \le \delta_{k'}$ for $k \le k'$, and $\eta \in (0,1)$ under $0 < \delta_{4k} < \sqrt2 - 1$.

Significance

The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once $m$ is of order $k\max(n,p)$) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every $k$-rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best $k$-rank approximation error in the nuclear norm.

Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.

Difficulty

The obvious argument would bound $\|H_1\|_*$ directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element $X$ has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to $X$, or to $H_2$, as a whole, and the constant $\eta$ depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.

Formalization scope

• Real matrices Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. $X^*$ is $X^{\top}$ and $\langle\cdot,\cdot\rangle$ is traceInner.
• Measurement map by matrices: $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$ (observationOp); $\|\mathcal S(X)\|^2_{\ell_2^m}$ is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.
• The squared RIP constant of Definition 1.1, defined as the infimum of the admissible $\delta \ge 0$ (attained, never a junk value), for every $k \in \mathbb N$; the page's range $1 \le k \le n$ is dropped because the goal uses $\delta_{4k}$ with $4k$ possibly larger than $n$. The unsquared constant $(1-\delta)\|X\|_F \le \|\mathcal S(X)\| \le (1+\delta)\|X\|_F$ used by other formalizations is a different quantity and is not used.
• Positivity $\delta_{4k} > 0$ is a hypothesis of the goal: it is Definition 1.1's own "$\delta_k > 0$", and without it $\eta = 0 \notin (0,1)$.
• No n ≤ p assumption: the proof does not use it.
• The block decomposition milestone states the page's explicit construction, with a general (not necessarily diagonal) top-left block, and without the unused hypothesis $X \in \ker\mathcal S$.
• The shelling bound is stated in its vector form for every block; the page writes "for $j \ge 2$" but display (6.7) uses it for every $j \ge 1$.

A formalization that proved only $\eta < 1$, or only the existence of some decomposition without the bound $\|H_1\|_* \le \eta\|H_2\|_*$, or that defined $\delta_k$ as any admissible constant rather than the smallest one, would not be this mission's goal.

Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.

Selected references

• M. Fornasier, H. Rauhut, R. Ward, Low-rank matrix recovery via iteratively reweighted least squares minimization, SIAM J. Optim. 21(4), 2011; read as arXiv:1010.2471v4. https://arxiv.org/abs/1010.2471
• E. J. Candès, Y. Plan, Tight oracle inequalities for low-rank matrix recovery from a minimal number of noisy random measurements, IEEE Trans. Inf. Theory 57(4), 2011. https://doi.org/10.1109/TIT.2011.2111771
• 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
• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Trans. Inf. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
• E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Math. Acad. Sci. Paris 346, 2008. https://doi.org/10.1016/j.crma.2008.03.014

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

Monotone variational inequalities (v.i.) cover convex minimization, convex–concave saddle-point problems, Nash equilibria of convex games and complementarity problems. Matrix games and other large saddle-point problems are typical cases. At large scale, first-order methods that use only values of the operator and simple auxiliary minimizations are the practical tool. The paper's introduction (pp. 229–231) contrasts this with the black-box lower bound of order $1/\epsilon^2$ evaluations for nonsmooth Lipschitz minimization, and with Nesterov's smoothing method (2005), which reaches $O(1/t)$ for structured saddle-point objectives. The paper states that its $O(1/t)$ complexity estimate is new, to the author's knowledge, even in the Euclidean case, where the scheme is Korpelevich's extragradient method of 1976.

A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15(1):229–251, 2004 (doi:10.1137/S1052623403425629), introduced what is now called the mirror-prox method. It showed that two prox steps per iteration give an ergodic error of order $1/N$ when the operator is Lipschitz continuous, and that the bound holds in an arbitrary norm, adapted to the geometry of the feasible set by a distance-generating function. The method and its analysis underlie later work on smooth saddle-point problems, including Nesterov's dual extrapolation and Juditsky–Nemirovski–Tauvel's stochastic mirror-prox (2011).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$, not necessarily Euclidean. Dual vectors $\xi$ act on $z\in E$ by $\langle\xi,z\rangle$, and the conjugate norm is $\|\xi\|_*=\max_{\|z\|\le1}\langle\xi,z\rangle$. Let $Z\subseteq E$ be nonempty, convex and compact.

The operator $F$ maps $Z$ to dual vectors and satisfies (2.1): it is $L$-Lipschitz, $\|F(z)-F(z')\|_*\le L\|z-z'\|$, and monotone, $\langle F(z)-F(z'),z-z'\rangle\ge0$, for all $z,z'\in Z$. A solution of the v.i. is a point $z_*\in Z$ with $\langle F(z),z_*-z\rangle\le0$ for all $z\in Z$. The accuracy of a candidate $\bar z\in Z$ is

$$\epsilon(\bar z)=\max_{u\in Z}\langle F(u),\bar z-u\rangle .$$

The distance-generating function $\omega:Z\to\mathbb R$ is continuously differentiable on $Z$ and strongly convex with modulus $\alpha>0$ in the form (2.2): $\langle\omega'(z)-\omega'(w),z-w\rangle\ge\alpha\|z-w\|^2$. The prox-mapping is

$$P_z(\xi)=\operatorname*{argmin}_{w\in Z}\big[\omega(w)+\langle\xi-\omega'(z),w\rangle\big],$$

and the constant $\Theta(z_0)=\max_{z\in Z}[\omega(z)-\omega(z_0)-\langle\omega'(z_0),z-z_0\rangle]$ measures how far $Z$ extends from the starting point $z_0$ in the geometry of $\omega$.

The basic implementation fixes the stepsize $\gamma=\alpha/(\sqrt2L)$ (3.2). At step $t$ it computes $w_{t,1}=P_{z_{t-1}}(\gamma F(z_{t-1}))$ and checks the test (3.4),

$$\langle\gamma F(a),a-b\rangle+\omega(z_{t-1})+\langle\omega'(z_{t-1}),b-z_{t-1}\rangle-\omega(b)\le0,$$

for $(a,b)=(z_{t-1},w_{t,1})$. If the test passes, $w_t=z_{t-1}$ and $z_t=w_{t,1}$. Otherwise $w_t=w_{t,1}$ and $z_t=P_{z_{t-1}}(\gamma F(w_{t,1}))$. The output after $N$ steps is the average $z^N=\frac1N\sum_{t=1}^Nw_t$ of the points $w_t$.

Formalization targets

Goal: Theorem 3.2 (p. 239), variational-inequality form

For every run of the basic implementation, (3.4) holds at every step, so two inner iterations always suffice, and for every $N\ge1$

$$\epsilon(z^N)\le\frac{\sqrt2\,\Theta(z_0)\,L}{\alpha N}.\tag{3.9}$$

Milestones, in the order of the proof

1. Lemma 2.1 (2.5), p. 232: $H_u(P_z(\xi))-H_u(z)\le\langle\xi,u-P_z(\xi)\rangle+[\omega(z)+\langle\omega'(z),P_z(\xi)-z\rangle-\omega(P_z(\xi))]$, and the bracket is $\le0$. Here $H_u(z)=\Omega(\omega'(z))-\langle\omega'(z),u\rangle$ and $\Omega$ is the Legendre transform of $\omega|_Z$.
2. (2.15), p. 235: one step of the relaxed conceptual prox-method satisfies $\langle\gamma_tF(w_t),w_t-u\rangle\le H_u(z_{t-1})-H_u(z_t)+\epsilon_t$.
3. Proposition 2.2(ii), p. 234: $\epsilon(z^N)\le(\Theta(z_0)+\sum_t\epsilon_t)/\sum_t\gamma_t$ for the relaxed method (2.11).
4. Lemma 3.1 (3.7.a), p. 238: $\|w-z_+\|\le\alpha^{-1}\gamma\|\xi-\eta\|_*$.
5. Lemma 3.1 (3.7.c), p. 238: $\delta\le\epsilon$.
6. Lemma 3.1 (3.7.d), p. 238: $\epsilon\le\alpha^{-1}\gamma^2\|\xi-\eta\|_*^2-\frac\alpha2[\|w-z\|^2+\|w-z_+\|^2]$.
7. The display of the proof of Theorem 3.2, p. 239: with $\gamma=\alpha/(\sqrt2L)$, the second inner iterate always passes (3.4).

Lemma 2.1 (2.4), Lemma 3.1 (3.7.b) and Remark 2.3 are also stated as companion theorems.

Significance

The theorem gives an $O(1/N)$ bound for monotone Lipschitz v.i. and for smooth convex–concave saddle points at a cost of two operator evaluations and two prox problems per step. With a distance-generating function adapted to $Z$, the paper derives rates that are, in its words, nearly dimension-independent under favorable circumstances, for matrix games, eigenvalue minimization and the Lovász capacity number (§5). In the Euclidean case $\omega=\frac12\|\cdot\|_2^2$ the method is Korpelevich's extragradient method, so the theorem also gives an ergodic $O(1/N)$ rate for that method.

The result is proved in the paper; no machine-checked proof of it is known. The platform has a formalized statement of mirror prox for minimization of a smooth convex function (Bubeck's Theorem 4.4), which uses a mirror map on an open set and a function-value gap. It does not cover operators, the v.i. accuracy measure or a prox-mapping over a compact set. This mission produces the general v.i. version, with an arbitrary norm and a distance-generating function defined only on $Z$.

Difficulty

The algebra of each step is short. The work is in three places. First, the first-order optimality conditions of the constrained prox problems, (2.6) and (3.8), must be derived when $\omega'$ is only a derivative within $Z$, and $Z$ may have empty interior. Second, (3.7.d) needs the function-value form of strong convexity, $\omega(w)\ge\omega(z)+\langle\omega'(z),w-z\rangle+\frac\alpha2\|w-z\|^2$, which must be derived from the monotonicity form (2.2) along segments of $Z$. Third, the telescoping of (2.15) uses the identity $\Omega(\omega'(z))=\langle\omega'(z),z\rangle-\omega(z)$ for $z\in Z$, and the passage from the weighted sum to the average uses monotonicity of $F$.

The natural first idea is to prove that the inner map $w\mapsto P_z(\gamma F(w))$ is a contraction, observation (3.1), and iterate it to a fixed point. That gives only a geometric number of inner steps, not two. The two-step bound comes from Lemma 3.1, which decouples the two prox steps and compares them through strong convexity.

Formalization scope

Dual vectors are continuous linear functionals E →L[ℝ] ℝ on a finite-dimensional normed space E, and $\|\cdot\|_*$ is the operator norm. This is equivalent to the paper's Euclidean space with a second norm. $Z$ is assumed convex, compact and nonempty in every item. $\omega$ has a derivative within $Z$ that is continuous on $Z$, and (2.2) is assumed in the monotonicity form. The prox-mapping is the relation "$v\in U$ minimizes $\omega(y)+\langle\xi-\omega'(z),y\rangle$ over $U$". $\Omega$ and $\Theta$ are suprema over the image of $Z$, which are maxima under these assumptions. The paper's indices are kept: z 0 is $z_0$, and step $t+1$ goes from z t to w (t+1) and z (t+1).

Disclosed choices: $L>0$ and $N\ge1$ are hypotheses, because (3.2) and (3.9) divide by them. The termination test (2.8) is not modelled, so runs never stop; this only adds runs. The basic implementation's inner loop is cut at $s=2$, which is what the goal's first claim justifies. The bound on $\epsilon(z^N)$ is stated for every $u\in Z$, which is equivalent to the bound on the maximum. Items that use only monotonicity of $F$, or no property of $F$, do not assume the rest of (2.1).

The goal quantifies over every run, and a sorry-free sanity file exhibits a run on $Z=[0,1]$, so the run relation is not empty. The average is over the $w_t$, not the $z_t$. The suprema are taken over compact nonempty $Z$ with continuous $\omega$, so they are not junk values. The saddle-point form (3.10), the bound (2.14) and Theorems 4.1–4.2 are not posed.

Useful contributions: optimality conditions for minimizers of functions differentiable within a convex set; the function-value form of strong convexity derived from (2.2); and the Legendre-transform identity. All three are reusable for other mirror-descent and prox-method analyses.

Selected references

• A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15(1):229–251, 2004. https://doi.org/10.1137/S1052623403425629
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12:747–756, 1976.
• Yu. Nesterov, Dual extrapolation and its applications to solving variational inequalities and related problems, Math. Program. 109:319–344, 2007. https://doi.org/10.1007/s10107-006-0034-z
• A. Juditsky, A. Nemirovski, C. Tauvel, Solving variational inequalities with stochastic mirror-prox algorithm, Stochastic Systems 1(1):17–58, 2011. https://doi.org/10.1214/10-SSY011
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8(3–4):231–357, 2015, §4.5. https://doi.org/10.1561/2200000050

Motivation

Robust regression guards a linear model against errors in the data matrix. The observations $b \in \mathbb R^n$ are fitted by $Ax$, but the features (the columns $a_1,\dots,a_m$ of $A$) are only known up to a disturbance $\Delta A$ from an uncertainty set $\mathcal U$. The robust estimator minimizes the worst-case residual,

$$\min_{x \in \mathbb R^m}\ \max_{\Delta A \in \mathcal U} \|b - (A+\Delta A)x\| .$$

Xu, Caramanis and Mannor (arXiv:0811.1790v1; IEEE Trans. Inf. Theory 56(7), 2010) showed that when each column is perturbed independently within a Euclidean ball of radius $c_i$, this problem is exactly the weighted $\ell_1$-regularized problem $\min_x \|b - Ax\|_2 + \sum_i c_i|x_i|$, an un-squared Lasso (their Theorem 1, the subject of the first mission of this series). Robustness then explains regularization: the penalty is the price of the worst disturbance.

Section III of the paper asks which regularizers arise when the disturbances of different features are coupled, that is, when a single budget limits all columns jointly. The answer it gives is that every norm-based regularizer arises this way: a norm budget on the vector of column-disturbance sizes produces the dual norm as the penalty. This links robust optimization (Ben-Tal, El Ghaoui, Nemirovski 2009) and regularized estimation, and it recovers the robust least-squares formulation of El Ghaoui and Lebret (1997) as the Euclidean special case.

Setting

Fix $n \ge 1$, $m \ge 0$, and an arbitrary norm $\|\cdot\|_a$ on $\mathbb R^n$. The data are the columns $a_1,\dots,a_m \in \mathbb R^n$ of $A$ and the response $b \in \mathbb R^n$; for $x \in \mathbb R^m$, $Ax = \sum_i x_i a_i$. A disturbance is $\Delta A = (\delta_1,\dots,\delta_m)$ with $\delta_i \in \mathbb R^n$; the perturbed matrix $A + \Delta A$ has columns $a_i + \delta_i$. For an uncertainty set $\mathcal U$ the robust objective is

$$R_{\mathcal U}(x) = \sup_{\Delta A\in\mathcal U} \|b - (A+\Delta A)x\|_a \in [-\infty,+\infty].$$

Three families of uncertainty sets appear.

1. Feature-wise (Theorem 3): for budgets $c_i \ge 0$, $\mathcal U_a = \{(\delta_1,\dots,\delta_m) : \|\delta_i\|_a \le c_i\}$.
2. Coupled (p. 6): for functions $f_1,\dots,f_k:\mathbb R^m\to\mathbb R$, $\mathcal U' = \{(\delta_1,\dots,\delta_m) : f_j(\|\delta_1\|_a,\dots,\|\delta_m\|_a) \le 0,\ j=1,\dots,k\}$, with the budget set $\mathcal Z = \{z \in \mathbb R^m : f_j(z) \le 0\ \forall j,\ z \ge 0\}$.
3. Norm budget (Corollary 1): for a norm $\|\cdot\|_s$ on $\mathbb R^m$ and $l \ge 0$, $\mathcal U' = \{(\delta_1,\dots,\delta_m) : \|(\|\delta_1\|_a,\dots,\|\delta_m\|_a)\|_s \le l\}$. The dual norm is $\|y\|_s^* = \sup\{y^\top z : \|z\|_s \le 1\}$. A norm is absolute if $\|(|z_1|,\dots,|z_m|)\|_s = \|z\|_s$ for all $z$.

A fourth, polytope set, $\{(\delta_1,\dots,\delta_m) : \exists c \ge 0,\ Tc \le s,\ \|\delta_j\|_a \le c_j\}$ for $T \in \mathbb R^{k\times m}$, $s\in\mathbb R^k$, is the subject of Corollary 2. Write $|x| = (|x_1|,\dots,|x_m|)$.

Formalization targets

Goal: Corollary 1 (p. 7)

For an absolute norm $\|\cdot\|_s$ and $l \ge 0$, for every $x \in \mathbb R^m$ the worst case over the norm-budget set is attained and

$$\max_{\Delta A\in\mathcal U'} \|b-(A+\Delta A)x\|_a = \|b - Ax\|_a + l\,\|x\|_s^*,$$

and the robust problem and $\min_x \|b-Ax\|_a + l\|x\|_s^*$ have the same minimizers.

Milestone: Theorem 3 (p. 6)

For $c \ge 0$ and every $x$: $\max_{\Delta A\in\mathcal U_a}\|b-(A+\Delta A)x\|_a = \|b-Ax\|_a + \sum_i c_i|x_i|$, attained, with the same minimizers.

Milestone: Eq. (13) (proof of Theorem 4, Appendix B, p. 19)

For every $x$, in the extended reals,

$$\sup_{\Delta A\in\mathcal U'} \|b-(A+\Delta A)x\|_a = \|b-Ax\|_a + \sup_{c\in\mathcal Z} |x|^\top c .$$

Milestone: Corollary 2 (p. 7)

If some $c \ge 0$ has $Tc \le s$, then for every $x$ the worst case over the polytope set equals $\|b-Ax\|_a + \inf\{s^\top\lambda : x \le T^\top\lambda,\ -x\le T^\top\lambda,\ \lambda\ge0\}$ (both sides $+\infty$ when the constraints are infeasible), the infimum is attained when feasible, and robust minimizers are exactly the $x$-parts of optimal solutions of that linear program.

The paper's general result, Theorem 4 (p. 6), expresses the coupled robust problem through a Lagrangian function $v(\lambda,\kappa,x)$ under the assumption that $\mathcal Z$ has nonempty relative interior. The mission does not pose it: that assumption is not Slater's condition, and the statement fails without one (an explicit counterexample with $\mathcal Z = \{0\}\times[0,\infty)$ is recorded in the series plan). The mission poses the decomposition (13), on which Theorem 4 rests, and the two corollaries, which are true as stated under the readings below.

Significance

The result. Corollary 1 says that any norm penalty $l\|x\|_s^*$ is the worst-case cost of column disturbances whose sizes are jointly bounded in the dual norm. Taking $\|\cdot\|_s = \ell_\infty$ gives the $\ell_1$ penalty (budget per column), $\ell_1$ gives $\ell_\infty$ (a shared budget), and both Euclidean gives the Frobenius-ball model of robust least squares. Corollary 2 shows that polytope budgets keep the problem a linear program apart from the loss, which allows modeling, for instance, corruption of an unknown subset of features. Eq. (13) is the common reduction behind these: the coupled worst case is the uncoupled one maximized over the admissible budget vectors.

Formalizing it. None of these statements has a machine-checked proof. The mission makes precise two points the paper leaves implicit: which "symmetric" norms the corollary is true for, and in what sense "max" holds when the budget set is empty or unbounded. The finished development is a self-contained library of worst-case residual identities for arbitrary norms on finite-dimensional or general normed spaces. Related platform items, credited and not reused: SPOBounds.StronglyConvex.dual_norm_ball_max (maximum of a linear functional over a norm ball, with the continuous-dual norm), and RobustLS.Unstructured.worst_case_residual_closed_form (El Ghaoui–Lebret, which perturbs $[A\ b]$ in a Frobenius ball, a different set).

Difficulty

The upper bound of every identity is a triangle inequality. The content is in the matching lower bound: a disturbance must be exhibited that aligns all perturbed columns with the residual direction, and in (13) each column disturbance must have norm exactly $c_i$, including columns with $x_i = 0$, which is where $n \ge 1$ enters. The paper's first line of the proof of (13) rewrites $\mathcal U'$ as $\{\Delta A : \exists c \in \mathcal Z,\ \|\delta_i\|_a \le c_i\}$; that set identity is false unless $\mathcal Z$ is downward closed, so the obvious route through it does not work for (13) as stated. For Corollary 1 the remaining step is the identity $\sup\{|x|^\top c : c\ge0,\ \|c\|_s\le l\} = l\|x\|_s^*$, which needs the absolute property and fails for norms that are only permutation invariant. For Corollary 2 the remaining step is linear programming duality, which Mathlib does not yet provide in this form.

Formalization scope

$(\mathbb R^n, \|\cdot\|_a)$ is an arbitrary real normed space $E$ with Nontrivial E (the paper's implicit $n\ge1$); finite dimension is not imposed, a harmless generalization. Columns are a family a : Fin m → E, disturbances δ : Fin m → E, coefficients Fin m → ℝ, and $Ax = \sum_i x_i \cdot a_i$. Explicit readings:

1. The robust objective is a supremum over the uncertainty set, computed in EReal; it is never defined by its closed form. "Max" is stated as IsGreatest of the set of residual values (attained) in Theorem 3 and Corollary 1, where the maximum exists, and as an EReal supremum in (13) and Corollary 2, where it need not.
2. "Is equivalent to" / "the resulting regularized regression problem is" means: equal objectives at every $x$ and equal sets of minimizers. Existence of a minimizer is not claimed.
3. "Symmetric norm" is read as absolute; $\|\cdot\|_s$ is a Mathlib Seminorm on Fin m → ℝ with $N z = 0 \Rightarrow z = 0$ (the type already carries the sup norm, so the notation $\|\cdot\|$ is not used for it). The dual norm is a real sSup of $\{y^\top z : N z \le 1\}$, a nonempty set that is bounded above because $N$ is a norm on $\mathbb R^m$.
4. $l \ge 0$ is added to Corollary 1, and feasibility of $c\ge0$, $Tc\le s$ to Corollary 2; without them the sets are empty.
5. Eq. (13) is stated for $\mathcal U'$ as defined on p. 6 (not through the paper's set rewriting); the convexity of the $f_j$ is kept as the paper's standing assumption and is not used.

A trivializing formalization is ruled out: the robust objective is the EReal supremum (or the residual-value set) over the uncertainty set, so no identity holds by unfolding, and no real sSup junk value enters a robust objective. Welcome contributions: the explicit worst-case disturbance in an arbitrary normed space, the absolute-norm duality lemma, and a finite-dimensional LP strong duality theorem, each reusable beyond this mission.

Selected references

• H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Transactions on Information Theory 56(7):3561–3574, 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM Journal on Matrix Analysis and Applications 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x