Convex Optimization

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality (LMI) $F(x) = F_0 + \sum_{i=1}^m x_iF_i \succeq 0$. SDPs model problems in control, combinatorial optimization, statistics and engineering design, and they are solved efficiently by interior-point methods. In applications the data $F_0,\dots,F_m$ are rarely known exactly: they come from measurements, from linearized models, or from rounding. A solution that is optimal for the nominal data may violate the constraint for data that differ only slightly.

El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for robust solutions: points $x$ that satisfy the constraint for every admissible value of an unknown but bounded perturbation, and among them one that minimizes $c^Tx$. Their paper, together with the contemporaneous work of Ben-Tal and Nemirovski on robust convex optimization (Math. Oper. Res. 23(4), 1998), founded robust semidefinite programming. The perturbation model they use, the linear-fractional representation (LFR), is the standard uncertainty model of robust control, where the same exact reformulation appears as the multiplier characterization of quadratic stability under norm-bounded uncertainty.

This mission formalizes the first main result of the paper: when the perturbation is full (an arbitrary matrix of bounded spectral norm), the robust problem is exactly an SDP with one extra scalar variable.

Setting

Fix natural numbers $m, n, p, q$ and a decision vector $x \in \mathbb{R}^m$. The data are:

• symmetric matrices $F_0,\dots,F_m \in \mathbb{R}^{n\times n}$, defining the affine map $F(x) = F_0 + \sum_i x_iF_i$;
• matrices $R_0,\dots,R_m \in \mathbb{R}^{q\times n}$, defining $R(x) = R_0 + \sum_i x_iR_i$;
• fixed matrices $L \in \mathbb{R}^{n\times p}$ and $D \in \mathbb{R}^{q\times p}$;
• a level $\rho > 0$.

For a matrix $X$, $\|X\|$ denotes its largest singular value (the spectral norm), and $X \succeq 0$ means that $X$ is symmetric positive semidefinite. A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$. The perturbed constraint matrix is the LFR (5)

$$\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,$$

which is well defined exactly when $\det(I - D\Delta) \neq 0$. For a linear subspace $\mathcal{D}$ of $\mathbb{R}^{p\times q}$, the robust feasible set (2) is

$$\mathcal{X}_\rho = \bigl\{x \in \mathbb{R}^m : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \mathbf{F}(x,\Delta) \text{ is well defined and } \mathbf{F}(x,\Delta) \succeq 0\bigr\},$$

and the robust SDP (4) is: minimize $c^Tx$ subject to $x \in \mathcal{X}_\rho$, for a given $c \in \mathbb{R}^m \setminus \{0\}$. In this mission $\mathcal{D} = \mathbb{R}^{p\times q}$, the full perturbation case, and the paper's standing assumption of §3.1 is $\|D\| < \rho^{-1}$.

Formalization targets

Goal: Theorem 3.1 (p. 36), as a set identity

Under $\rho > 0$, $\|D\| < \rho^{-1}$, $q \ge 1$ and $L \ne 0$, for every $x \in \mathbb{R}^m$,

$$x \in \mathcal{X}_\rho \iff \exists\,\tau \in \mathbb{R}:\ \begin{bmatrix} F(x) - \tau LL^T & R(x)^T - \tau LD^T \\ R(x) - \tau DL^T & \tau(\rho^{-2}I - DD^T)\end{bmatrix} \succeq 0. \qquad (10)$$

The paper states that the robust SDP and a corresponding solution can be computed by solving the SDP "minimize $c^Tx$ subject to (10)" in the variables $(x, \tau)$. Both problems have the objective $c^Tx$, so the identity above, between $\mathcal{X}_\rho$ and the $x$-projection of the feasible set of (10), is the content of that sentence. A companion item states the solution correspondence explicitly: $x$ is optimal for the robust SDP if and only if $(x,\tau)$ is optimal for (10) for some $\tau$.

Milestones

1. Well-posedness (§3.1, p. 36). For $\rho > 0$: $\det(I - D\Delta) \ne 0$ for every $\Delta$ with $\|\Delta\| \le \rho$ if and only if $\|D\| < \rho^{-1}$.
2. Lemma 3.1 (p. 36). For $F = F^T$, $q \ge 1$ and $L \ne 0$: $\det(I - D\Delta) \ne 0$ and $F + L\Delta(I - D\Delta)^{-1}R + R^T(I - D\Delta)^{-T}\Delta^TL^T \succeq 0$ for every $\|\Delta\| \le 1$ if and only if $\|D\| < 1$ and some scalar $\tau$ satisfies

$$\begin{bmatrix} F - \tau LL^T & R^T - \tau LD^T \\ R - \tau DL^T & \tau(I - DD^T)\end{bmatrix} \succeq 0.$$

The paper cites the S-procedure as the classical result behind Lemma 3.1; it is already proved on the platform (ConvexOptimization.s_procedure) and is included as a reference item.

Significance

The robust feasible set is defined by infinitely many matrix inequalities, one per perturbation, each rational in $\Delta$; in general such a set is convex but has no tractable description, and the paper notes that the structured version of the problem is NP-hard. Theorem 3.1 shows that for full perturbations nothing is lost by replacing that semi-infinite constraint with a single LMI of size $n + q$ in one extra variable. Consequences: the robust problem is solved by a standard SDP solver; the largest admissible perturbation level is a generalized eigenvalue problem; and the exact result is the benchmark against which the paper's sufficient conditions for structured perturbations (Theorem 3.2) and its closed-form counterparts for unstructured perturbations (Theorem 5.1) are measured.

The result is proved in the paper (from the S-procedure, with the details deferred to a cited report). To the best of available knowledge it has no machine-checked proof. The mission produces a formal statement of the LFR model and of the robust feasible set that later missions on robust SDPs can reuse, a formal proof of the well-posedness condition, and a formal proof of the exact reformulation built on the platform's S-procedure. Formalizing it also records two points the printed statement leaves implicit: the result needs $L \ne 0$ and a nonempty perturbation output dimension $q \ge 1$.

Difficulty

The direction from the LMI to robust feasibility is elementary. The converse is the substance: robust feasibility is a statement about a continuum of perturbations, each entering rationally, and testing the LMI against finitely many extreme perturbations does not produce a multiplier $\tau$. The exactness of the reformulation rests on a lossless certificate for an implication between quadratic inequalities, which holds only under a strict feasibility condition; that condition is where $L \ne 0$ enters, and without it the lemma is false. The well-posedness milestone requires showing that $\|D\| < \rho^{-1}$ is also necessary, which is not a norm estimate but needs a perturbation that makes $I - D\Delta$ singular.

Formalization scope

Matrices are Mathlib Matrix (Fin a) (Fin b) ℝ. The affine maps are given by coefficient lists indexed by Fin (m + 1), the constant term first. The norm on matrices is the $\ell^2$ operator norm, opened with open scoped Matrix.Norms.L2Operator; it is the largest singular value, and no other matrix norm is used. $X \succeq 0$ is Matrix.PosSemidef, which includes symmetry. Block matrices are Matrix.fromBlocks over the index type Fin n ⊕ Fin q, with $R(x)^T - \tau LD^T$ top-right and $R(x) - \tau DL^T$ bottom-left. Mathlib's matrix inverse returns $0$ at a singular matrix, so the condition $\det(I - D\Delta) \ne 0$ appears in the robust feasible set in the same universally quantified clause as positive semidefiniteness, as the paper's "well defined" requires; dropping it, or using an entrywise matrix norm, would change the set and is excluded.

Readings and corrections of the printed statements:

• "The RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the identity of $\mathcal{X}_\rho$ with the $x$-projection of the feasible set of (10), for every $x$, together with the solution correspondence item. A statement of equal optimal values alone would be weaker and is not used.
• Correction: $L \ne 0$ is added to Lemma 3.1 and Theorem 3.1. The printed statements fail for $L = 0$: with $n = p = q = 1$, $F = 0$, $L = 0$, $D = 0$, $R = 1$, the perturbation does not enter, so the robust condition holds, while the LMI reads $\begin{bmatrix}0 & 1\\1 & \cdot\end{bmatrix} \succeq 0$, which is infeasible.
• $q \ge 1$ makes "matrices of appropriate size" explicit; for $q = 0$ the lower-right block is empty and the equivalence fails.
• The standing assumptions $\rho > 0$ (§3) and $\|D\| < \rho^{-1}$ (§3.1) are hypotheses of the goal. In Lemma 3.1, $\|D\| < 1$ is part of the conclusion, as printed, and $\tau$ carries no sign constraint, as printed.
• The paper's standing assumption that the nominal problem is feasible ($\mathcal{X}_0 \ne \emptyset$) is not needed for the identity and is not added.

Welcome contributions: proofs of the well-posedness milestone (a spectral-norm and singular-vector argument, reusable wherever $I - D\Delta$ must be invertible); of Lemma 3.1 from the S-procedure (the reachability lemma for norm-bounded perturbations is reusable in robust control); of the goal from Lemma 3.1 by rescaling; and general lemmas on the spectral norm of rank-one matrices and on Schur complements of block matrices.

Selected references

• L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
• A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B.2 (the S-procedure). https://web.stanford.edu/~boyd/cvxbook/

Motivation

Many convex sets that appear in optimization have complicated descriptions in their own space but simple descriptions as projections of higher-dimensional sets. A polytope with exponentially many facets can be the shadow of a polyhedron with polynomially many; the unit disk is the projection of a slice of the cone of $2\times 2$ positive semidefinite matrices. Such a representation, a lift, turns linear optimization over the original set into a linear or semidefinite program over the lifted one, so the size of the smallest lift measures how hard the set is for conic optimization.

For polytopes and polyhedral lifts, Yannakakis (Yannakakis 1991) showed that the minimal size of a lift equals the nonnegative rank of the polytope's slack matrix. This turned questions about extended formulations into questions about matrix factorizations, and it is the basis of the lower bounds of Fiorini, Massar, Pokutta, Tiwary and de Wolf (2012) for the cut, stable set and traveling salesman polytopes. Lift-and-project hierarchies (Sherali–Adams, Lovász–Schrijver, Lasserre) all produce lifts to nonnegative orthants or positive semidefinite cones, so a criterion for the existence of a lift is also a criterion for when such a hierarchy can succeed.

Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 38(2), 2013) extended Yannakakis' theorem from polytopes and polyhedral cones to arbitrary convex bodies and arbitrary closed convex cones. Their Theorem 2.4 is the target of this mission.

Timeline:

• 1991, Yannakakis: polytopes, polyhedral lifts, nonnegative factorizations of the slack matrix.
• 2012, Fiorini, Massar, Pokutta, Tiwary, de Wolf: superpolynomial lower bounds on polyhedral lifts via nonnegative rank; a positive semidefinite analogue for polytopes.
• 2011/2013, Gouveia, Parrilo, Thomas: convex bodies and general closed convex cones (Theorem 2.4), with psd rank as the semidefinite analogue of nonnegative rank.

Setting

Throughout, $\mathbb R^k$ carries the Euclidean inner product $\langle\cdot,\cdot\rangle$.

A convex body is a set $C \subseteq \mathbb R^n$ that is convex, compact, and contains the origin in its interior. Its polar is

$$C^\circ = \{\, y \in \mathbb R^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.$$

A point $p \in C$ is an extreme point if $p = (p_1+p_2)/2$ with $p_1,p_2\in C$ forces $p_1 = p_2 = p$; $\operatorname{ext}(C)$ is the set of extreme points. The slack operator of $C$ is

$$S_C : \operatorname{ext}(C)\times\operatorname{ext}(C^\circ) \to \mathbb R, \qquad S_C(x,y) = 1 - \langle x,y\rangle .$$

It is nonnegative, and for a polytope it is the slack matrix: rows indexed by vertices, columns by facet normals.

Let $K \subseteq \mathbb R^m$ be a full-dimensional closed convex cone: closed, convex, closed under nonnegative scaling, with nonempty interior. Its dual is $K^* = \{y : \langle x,y\rangle \ge 0 \ \forall x\in K\}$.

• A $K$-lift of $C$ is $Q = K\cap L$, where $L\subseteq\mathbb R^m$ is an affine subspace and $\pi:\mathbb R^m\to\mathbb R^n$ is a linear map with $C = \pi(K\cap L)$. The lift is proper if $L$ meets the interior of $K$ (Definition 2.1).
• $S_C$ is $K$-factorizable if there are maps, not necessarily linear, $A:\operatorname{ext}(C)\to K$ and $B:\operatorname{ext}(C^\circ)\to K^*$ with $S_C(x,y) = \langle A(x), B(y)\rangle$ for all $(x,y)$ (Definition 2.2).

In Lean these are IsConvexBody, IsClosedConvexCone, HasLift, HasProperLift and SlackFactorizable in the namespace ConeLifts.Factorization, together with the series' shared ConeLifts.Shared.polar and ConeLifts.Shared.dualCone.

Formalization targets

Goal: Theorem 2.4

For $n \ge 1$, a convex body $C\subseteq\mathbb R^n$ and a full-dimensional closed convex cone $K\subseteq\mathbb R^m$:

$$\bigl(C \text{ has a proper } K\text{-lift} \Rightarrow S_C \text{ is } K\text{-factorizable}\bigr) \;\wedge\; \bigl(S_C \text{ is } K\text{-factorizable} \Rightarrow C \text{ has a } K\text{-lift}\bigr).$$

The two implications are not an equivalence: the forward one assumes properness, and the lift produced by the converse may be improper.

Milestones

In the order the paper's proof uses them:

1. (§2, p. 3) $C = \operatorname{conv}(\operatorname{ext} C)$ and $C^\circ = \operatorname{conv}(\operatorname{ext} C^\circ)$.
2. (proof, p. 4) For every $c\in\operatorname{ext}(C^\circ)$, $\max\{\langle c,x\rangle : x\in C\} = 1$, attained.
3. (proof, p. 4) If $C = \pi(K\cap L)$, $L = w_0 + L_0$ and $w_0\in\operatorname{int}K$, then for $c \in \operatorname{ext}(C^\circ)$

$$1 = \min\{\langle w_0, z\rangle : z - \pi^*(c)\in K^*,\ z\in L_0^\perp\},$$

with the minimum attained. 4. (proof, p. 5) For $L = \{(x,z) : 1-\langle x,y\rangle = \langle z, B(y)\rangle\ \forall y\in\operatorname{ext}(C^\circ)\}$ and its projection $L_K$ to $\mathbb R^m$: $0\notin L_K$. 5. (proof, p. 5) If $B$ maps into $K^*$, $z\in K$ and $(x,z)\in L$, then $x\in C$. 6. (proof, p. 5) For each $z\in K\cap L_K$ there is a unique $x_z$ with $(x_z,z)\in L$.

Significance

The result. Theorem 2.4 makes the existence of a lift of a convex body to a given cone a purely algebraic question about its slack operator. Every lower bound on lift size in the paper and its successors goes through it: the nonnegative-rank bounds for polytopes (Section 4 of the paper), the proof that the stable set polytope of an $n$-vertex graph has no lift to $\mathcal S^n_+$ (Section 5), and the later psd-rank literature. It also puts Yannakakis' theorem and its semidefinite analogue under a single statement.

Formalizing it. The theorem is proved on paper; no machine-checked version is known to exist. Formalizing it requires conic strong duality with dual attainment under a Slater condition, which Mathlib does not have, and finite-dimensional Krein–Milman for the polar body. The companion missions of this series (nonnegative-rank lower bounds; stable set polytopes and psd lifts) use the correspondence as their entry point.

Difficulty

The converse half is elementary once the extreme points of $C^\circ$ are known to generate it. The forward half is not: $B(c)$ must be an element of $K^*$ that certifies $\langle c, x\rangle \le 1$ on $C$ through the lift. A separating functional gives this certificate on $\pi(K\cap L)$, but writing it as $z - \pi^*(c)$ with $z \perp L_0$, $z - \pi^*(c)\in K^*$ and $\langle w_0,z\rangle = 1$ exactly is conic duality with a zero gap and an attained dual optimum. For closed convex cones the gap can be positive or the dual unattained unless a constraint qualification holds; this is why properness is assumed. Weak duality alone gives only $\ge 1$, and a dual sequence approaching $1$ does not yield a factor. The paper notes (p. 5) that, since the proof uses strong duality, it is not obvious how to remove properness for a general closed convex cone.

Formalization scope

Conventions fixed by the Lean statements:

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k); every pairing, in $S$, in $K^*$ and in the factorization, is its inner product.
• The polar is one-sided, $\langle x,y\rangle\le 1$; Mathlib's absolute polar is not used.
• A convex body is compact, convex, with $0$ in its interior. The paper's "full-dimensional convex body in $\mathbb R^n$" is read as including $n\ge 1$: for $n = 0$, $C = \{0\}$ has the proper $\mathbb R^m$-lift $\{0\}$ while $S_C(0,0) = 1$ cannot factor through $K^* = \{0\}$, so the forward half is false there. The goal and milestones 2–3 assume $1\le n$.
• $K$ is closed, convex, contains $0$ and is closed under nonnegative scaling; full-dimensionality is (interior K).Nonempty. Pointedness is not assumed.
• $L$ is a Mathlib AffineSubspace and $\pi$ a linear map; the lift condition is the set equality $C = \pi(K\cap L)$.
• $A, B$ are total functions $\mathbb R^n\to\mathbb R^m$ constrained only on $\operatorname{ext}(C)$, resp. $\operatorname{ext}(C^\circ)$, which is equivalent to maps out of the extreme points. They are not required to be linear or continuous.
• Milestone 3 is the second, substituted form of the paper's dual ($z = M^{\mathsf T}y$), stated with L.directionᗮ and LinearMap.adjoint π; minima and maxima are stated with IsLeast/IsGreatest, so attainment is part of every claim.

Trivializing readings are excluded: $\pi$ is linear, not an arbitrary function (with an arbitrary function every set is a "lift"); $L$ is an affine subspace, not an arbitrary set; and $B$ takes values in $K^*$, not $K$, which for a cone that is not self-dual would be a different and generally false statement.

Needed infrastructure: finite-dimensional Krein–Milman in the form $C = \operatorname{conv}(\operatorname{ext} C)$ for compact convex sets (Mathlib has the closure form); the bipolar theorem $(C^\circ)^\circ = C$ for closed convex $C\ni 0$ with the one-sided polar; compactness of $C^\circ$ when $0\in\operatorname{int} C$; and conic linear programming duality with a Slater point, including dual attainment. The last two are reusable well beyond this mission. Proofs of individual milestones, and of these general facts as separate lemmas, are welcome.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2, doi:10.1287/moor.1120.0575
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. doi:10.1016/0022-0000(91)90024-Y
• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Linear vs. semidefinite extended formulations: exponential separation and strong lower bounds, STOC 2012. arXiv:1111.0837

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$, $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$. For a matrix $X$, $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^n$, $L \in \mathbb R^{n\times N}$, $R_A \in \mathbb R^{N\times m}$, $R_b \in \mathbb R^N$, $D \in \mathbb R^{N\times N}$. For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

$$A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .$$

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

$$r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|$$

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$, and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

$$\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)$$

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$:

$$\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);$$ $$\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .$$

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$. Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$, where (40) is infeasible.

Milestones

1. Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$).
2. Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$, and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$.
3. §5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
4. §5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$. Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$. The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$, and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

• Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
• $\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$. It is false for every $\lambda$ when $r_{\mathcal D} = \infty$. No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$. Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
• $\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$.
• Corrections of the printed statements. (i) (40) must require $S \succ 0$. Without it, $N = n = m = 1$, $D = 2$, $L = 1$, $A = b = R_A = R_b = 0$, $x = 0$, $S = -1$, $G = 0$ satisfy (38) for every $\lambda > 1/3$, while $r_{\mathcal D} = \infty$. (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$, which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$, $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$, the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$. The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$. (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$.
• Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
• Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$, $G = 0$ for full $\mathcal D$, which part (b) produces).
• Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$, and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

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. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
• I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

Motivation

Least squares fits a model $Ax \approx b$ as if the data $(A, b)$ were exact. In practice they are measured, rounded or estimated, and the least-squares solution can be very sensitive to such errors. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to treat the errors as deterministic, unknown but bounded, and to choose $x$ minimizing the worst-case residual over all admissible data. For unstructured perturbations of $[A\ b]$ bounded in Frobenius norm this leads to a second-order cone program (missions I and II of this series).

In many applications the perturbations have a known structure: a Toeplitz matrix stays Toeplitz, a parameter enters several entries at once, or only some entries are uncertain. An unstructured bound then over-estimates the worst case. The paper's §4 treats perturbations that are affine in a parameter vector $\delta$ bounded in Euclidean norm, and shows that the resulting structured robust least-squares (SRLS) problem is still solved exactly, now by a semidefinite program (SDP). This model of uncertainty (an ellipsoid of affinely parametrized data) is the one later adopted as the basic uncertainty set of robust optimization; see Ben-Tal and Nemirovski, Math. Oper. Res. 23(4), 1998.

Setting

Vectors carry the Euclidean norm $\|v\| = \sqrt{v^Tv}$. Given matrices $A_0, A_1, \dots, A_p \in \mathbb{R}^{n\times m}$ and vectors $b_0, b_1, \dots, b_p \in \mathbb{R}^n$, define for every $\delta \in \mathbb{R}^p$

$$\mathbf A(\delta) = A_0 + \sum_{i=1}^p \delta_i A_i, \qquad \mathbf b(\delta) = b_0 + \sum_{i=1}^p \delta_i b_i .$$

For $\rho \ge 0$ and $x \in \mathbb{R}^m$ the structured worst-case residual is

$$r_S(\mathbf A, \mathbf b, \rho, x) = \max_{\|\delta\| \le \rho} \|\mathbf A(\delta)x - \mathbf b(\delta)\|,$$

and $x$ is an SRLS solution if it minimizes $r_S(\mathbf A, \mathbf b, \rho, \cdot)$ over $\mathbb{R}^m$. The paper takes $\rho = 1$ throughout §4 and writes $r_S(\mathbf A, \mathbf b, x)$.

For fixed $x$ let $M(x) = [A_1x - b_1\ \cdots\ A_px - b_p] \in \mathbb{R}^{n\times p}$ and

$$F = M(x)^TM(x), \qquad g = M(x)^T(A_0x - b_0), \qquad h = \|A_0x - b_0\|^2 .$$

Since $\mathbf A(\delta)x - \mathbf b(\delta) = (A_0x - b_0) + M(x)\delta$, the squared residual at $\delta$ is the quadratic function $h + 2g^T\delta + \delta^TF\delta$. Finally, for scalars $\lambda, \tau$,

$$\mathcal F(\lambda, \tau) = \begin{bmatrix} \lambda - \tau - h & -g^T \\ -g & \tau I - F \end{bmatrix}.$$

Formalization targets

Goal: Theorem 4.2

With $p \ge 1$ and $\rho = 1$, consider the SDP in $(\lambda, \tau, x)$

$$\text{minimize } \lambda \quad \text{subject to} \quad \begin{bmatrix} \lambda - \tau & 0 & (A_0x - b_0)^T \\ 0 & \tau I & M(x)^T \\ A_0x - b_0 & M(x) & I \end{bmatrix} \succeq 0. \tag{32}$$

The goal states that (a) for all $x$ and $\lambda$, some $\tau$ makes $(\lambda, \tau, x)$ feasible if and only if $r_S(\mathbf A, \mathbf b, x)^2 \le \lambda$; and (b) $(\lambda, \tau, x)$ is optimal for (32) if and only if $x$ is an SRLS solution, $\lambda = r_S(\mathbf A, \mathbf b, x)^2$, and $(\lambda, \tau, x)$ is feasible. This is the precise content of the paper's "the SRLS can be solved by computing an optimal solution of (32)".

Milestones

1. Lemma 2.1 (S-procedure), in two items: the multiplier condition is sufficient for every $p$; for $p = 1$ it is also necessary when $F_1(\zeta_0) > 0$ for some $\zeta_0$.
2. Eq. (28): $r_S(\mathbf A, \mathbf b, x)^2 = \max_{\delta^T\delta \le 1} [1;\delta]^T \begin{bmatrix} h & g^T \\ g & F\end{bmatrix} [1;\delta]$.
3. Eq. (29): for $\lambda \ge 0$, that quadratic form is $\le \lambda$ on the unit ball if and only if $\mathcal F(\lambda, \tau) \succeq 0$ for some $\tau$.
4. Theorem 4.1, first assertion: $r_S(\mathbf A, \mathbf b, x)^2 = \min\{\lambda : \exists \tau,\ \mathcal F(\lambda, \tau) \succeq 0\}$, the minimum attained.
5. §4.2, Schur-complement step: the matrix of (32) is positive semidefinite if and only if $\mathcal F(\lambda, \tau)$ is.

Significance

The result shows that a min–max problem over a nonconvex worst case (the inner problem maximizes a convex quadratic over a ball) is equivalent to a single convex SDP whose size is linear in $n$, $m$ and $p$, and hence solvable in polynomial time by interior-point methods. It covers as special cases the unstructured problem of §3, least squares with uncertainty in selected entries, and Toeplitz or otherwise patterned perturbations. The exactness contrasts with the next section of the paper, where the linear-fractional and $\ell_\infty$-bounded versions are in general only bounded from above, or shown NP-hard.

The result is proved in the paper; to the best of current knowledge it has not been formalized. The platform already has the one-constraint S-procedure (ConvexOptimization.s_procedure, proved, in a different sign and block convention); this mission adds the robust least-squares objects, the reduction to the S-procedure, the Schur-complement step, and the optimal-solution correspondence of Theorem 4.2. The worst-case residual and SDP (32) definitions are reusable by later robust-regression missions.

Difficulty

The obvious approach is to compute the inner maximum directly. The function $\delta \mapsto h + 2g^T\delta + \delta^TF\delta$ is convex, so its maximum over the unit ball is attained on the boundary, but it is not given by any closed-form expression in general, and maximizing a convex function is not a convex problem. Exactness therefore rests on the lossless S-procedure for one quadratic constraint, a nonconvex duality statement that fails for two or more constraints; the sufficient direction alone only yields an upper bound.

A second point is passing from "for fixed $x$" (Theorem 4.1) to "optimal over $x$" (Theorem 4.2): $\mathcal F(\lambda, \tau)$ is quadratic in $x$, and only the Schur-complement lift (32) is jointly affine in $(\lambda, \tau, x)$. The correspondence of optimal solutions must then be checked in both directions, including that the optimal $\lambda$ is the squared residual and not the residual.

Formalization scope

• Data are A0 : Matrix (Fin n) (Fin m) ℝ, A : Fin p → Matrix (Fin n) (Fin m) ℝ, b0 : Fin n → ℝ, b : Fin p → Fin n → ℝ; A i is the paper's $A_{i+1}$ (0-based index). Vectors live in Fin k → ℝ with the Euclidean norm written out as $\sqrt{\sum_i v_i^2}$, never Mathlib's sup norm.
• The maximum defining $r_S$ is sSup of the set of attained residuals over the closed ball; for $\rho \ge 0$ this set is nonempty and bounded, so sSup is the true maximum. The theorems use $\rho = 1$, as the paper does; the paper derives general $\rho$ by scaling and that is not stated here.
• Block matrices are Matrix.fromBlocks in the printed order (scalar block first: Unit ⊕ Fin p; for (32), (Unit ⊕ Fin p) ⊕ Fin n). "$\succeq 0$" is Mathlib's PosSemidef, which includes symmetry; all matrices here are symmetric by construction.
• $p \ge 1$ is assumed in (29), Theorem 4.1 and Theorem 4.2, although the paper does not state it: for $p = 0$ the block $\tau I$ is empty, $\tau$ is unconstrained, every $\lambda$ is feasible and both SDPs lose their meaning. Eq. (28), Lemma 2.1 and the Schur-complement step hold for every $p$ and are stated without it.
• Optimality in (32) is stated as feasibility plus $\lambda \le \lambda'$ for every feasible $(\lambda', \tau', x')$. A formalization that only proves existence of some feasible $\tau$, or only an inequality between the optimal values, is weaker than Theorem 4.2 and does not close the goal.
• Theorem 4.1's second and third assertions (the one-dimensional reformulation (30)–(31) and the worst-case perturbation) are not included: they use the notion "$(F, g)$-controllable", which the paper does not define.
• Useful infrastructure: Mathlib's Schur-complement lemmas (Matrix.PosSemidef.fromBlocks₂₂ and relatives in LinearAlgebra.Matrix.SchurComplement); the platform's ConvexOptimization.s_procedure and ConvexOptimization.single_constraint_quadratic_strong_duality with their definitions ConvexOptimization_quadraticForms, included as reference items. A bridge lemma between the platform's block convention and this mission's is a welcome contribution, as is a general-$\rho$ version.

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. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994 (the S-procedure, p. 24). https://doi.org/10.1137/1.9781611970777
• A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• I. Pólik and T. Terlaky, A Survey of the S-Lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

Motivation

The least-squares (LS) problem $\min_x \|Ax - b\|$ assumes that the data $A \in \mathbb{R}^{n\times m}$, $b \in \mathbb{R}^n$ are exact. In applications they rarely are: they come from measurements, from linearizations, or from models with neglected dynamics. A classical response is sensitivity analysis or regularization (Tikhonov), where a weight trades the size of the solution against the fit, and the choice of that weight is left to the user. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) take a deterministic view instead: the true data lie in a known ball around $(A, b)$, and the solution should minimize the residual it can be forced to have in the worst case over that ball. The paper shows that this robust least-squares (RLS) problem is solvable exactly, in the unstructured case by a second-order cone program (SOCP). The same worst-case idea, applied to regression, underlies the later equivalence between robustness and regularization (Xu, Caramanis and Mannor, 2009) and is a standard entry point to robust optimization (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009).

This mission formalizes the first main result of the paper, Theorem 3.1: the worst-case residual has a closed form, its minimizer is unique, and minimizing it is an SOCP.

Setting

Vectors carry the Euclidean norm $\|v\| = (\sum_i v_i^2)^{1/2}$. For a matrix $X$, $\|X\|_F = (\sum_{i,j} X_{ij}^2)^{1/2}$ is the Frobenius norm and $\|X\|$ the largest singular value, i.e. the smallest $c \ge 0$ with $\|Xv\| \le c\|v\|$ for all $v$.

Fix $A \in \mathbb{R}^{n\times m}$ and $b \in \mathbb{R}^n$. A perturbation is a pair $\Delta A \in \mathbb{R}^{n\times m}$, $\Delta b \in \mathbb{R}^n$, collected in the augmented matrix $\Delta = [\Delta A\ \Delta b] \in \mathbb{R}^{n\times(m+1)}$. For a bound $\rho \ge 0$ and $x \in \mathbb{R}^m$, the worst-case residual is (paper, eq. (1))

$$r(A,b,\rho,x) = \max_{\|[\Delta A\ \Delta b]\|_F \le \rho} \|(A+\Delta A)x - (b+\Delta b)\|,$$

and $x$ is an RLS solution if it minimizes $r(A,b,\rho,\cdot)$. The bound constrains the augmented matrix jointly, not $\Delta A$ and $\Delta b$ separately. The paper normalizes $\rho = 1$ and writes $r(A,b,x) = r(A,b,1,x)$. Finally, $[x;1] \in \mathbb{R}^{m+1}$ denotes $x$ stacked over $1$. In the Lean development these are RobustLS.Unstructured.eucNorm, frobNorm, specNorm, augment, stackOne, worstCaseResidual A b ρ x, its largest-singular-value variant worstCaseResidualSpec, and the SOCP constraint predicate SocpFeasible A b x λ τ.

Formalization targets

Goal: Theorem 3.1 (p. 1040)

For $n \ge 1$, every $A$, $b$:

$$r(A,b,x) = \|Ax-b\| + \sqrt{\|x\|^2+1} \quad \text{for all } x \in \mathbb{R}^m,$$

the problem $\min_{x \in \mathbb{R}^m} r(A,b,x)$ has exactly one solution $x_{\mathrm{RLS}}$, and it is the SOCP

$$\text{minimize } \lambda \quad\text{subject to}\quad \|Ax-b\| \le \lambda-\tau,\quad \|[x;1]\| \le \tau, \tag{15}$$

in the sense that $r(A,b,x)$ is the least $\lambda$ for which some $\tau$ makes $(x,\lambda,\tau)$ feasible.

Milestones

1. Eq. (16). Every perturbation with $\|[\Delta A\ \Delta b]\|_F \le 1$ has residual at most $\|Ax-b\| + \sqrt{\|x\|^2+1}$.
2. The worst-case perturbation. For a unit vector $u$ aligned with $Ax - b$ (arbitrary if $Ax = b$), the rank-one matrix $\Delta = u[x^T\ {-1}]/\sqrt{\|x\|^2+1}$ has $\|\Delta\|_F = \|\Delta\| = 1$ and attains the bound.
3. Spectral norm. The worst case over the larger ball $\|[\Delta A\ \Delta b]\| \le 1$ is the same value.
4. Strict convexity. $x \mapsto r(A,b,x)$ is strictly convex on $\mathbb{R}^m$.
5. The SOCP (15). For every $x$, $r(A,b,x)$ is the optimal $\lambda$ of (15) with $x$ fixed, and $x$ is an RLS solution exactly when it is the $x$-part of an optimal solution of (15).

Significance

The closed form replaces a maximization over a matrix ball of dimension $n(m+1)$ by two Euclidean norms. It shows that the RLS objective is the LS residual plus a penalty $\sqrt{\|x\|^2+1}$ that does not depend on $A$ or $b$, which is the starting point for the paper's Theorem 3.2 (the RLS solution is a Tikhonov-regularized LS solution with a data-dependent weight) and its analysis of continuity and conditioning. The SOCP formulation places the problem in the class solved by interior-point methods, at a cost the paper compares with one singular value decomposition of $A$. The spectral-norm statement says the worst case does not depend on which of the two standard matrix norms bounds the perturbation.

The result is proved in the paper; the proof is short. To the best of the planning survey (September 2026), no machine-checked proof exists, and Prove2Me has no statement about worst-case residuals or robust least squares. The mission produces a verified closed form that later missions of this series (Tikhonov form of the solution, structured and linear-fractional perturbations) and any formalization of robust regression can import.

Difficulty

The upper bound alone does not give the theorem: the statement is an equality, and the equality needs an explicit maximizer. The paper's printed maximizer is wrong by a sign: with $[x^T\ 1]$ in place of $[x^T\ {-1}]$ the perturbation does not attain the bound (for $A = 0$, $x = 0$, $b = e_1$ it gives residual $0$ instead of $2$), so a transcription of the printed proof fails. Two further points are silent in the paper. The operator norm of a rank-one matrix has to be computed from the definition of the largest singular value. Uniqueness of the minimizer needs existence first, which follows from growth of $r$ at infinity and is not stated. Working with the sSup definition of the worst case requires showing the set of residuals is bounded, which is milestone 1.

Formalization scope

• Dimensions are Fin n, Fin m; $A$ is Matrix (Fin n) (Fin m) ℝ, $b$ and $x$ are functions Fin n → ℝ, Fin m → ℝ. The augmented matrix $[\Delta A\ \Delta b]$ is indexed by Fin m ⊕ Unit, and so is $[x;1]$.
• Vector norms are the Euclidean norm written as $\sqrt{\sum_i v_i^2}$ (eucNorm), never Mathlib's ‖·‖ on Fin n → ℝ, which is the sup norm. The Frobenius norm and the largest singular value are explicit definitions (frobNorm, specNorm); specNorm is the infimum of admissible operator constants.
• The maximum in (1) is sSup of the set of attained residuals. For $\rho \ge 0$ the set is nonempty and bounded, so this is the true maximum; milestones 1 and 2 state the bound and the attaining perturbation directly, so no statement relies on the value of sSup on an unbounded set.
• The paper's normalization $\rho = 1$ is kept; general $\rho > 0$ follows from the scaling $\phi(A,b,\rho) = \rho\,\phi(A/\rho,b/\rho,1)$ the paper records on p. 1039 and is not a target.
• The goal assumes $n \ge 1$. For $n = 0$ the only perturbation is the empty matrix, the worst case is $0$, and the closed form fails; the paper's setting ($Ax \simeq b$ with data $b \in \mathbb{R}^n$) has $n \ge 1$. Milestones 3–5 carry the same hypothesis.
• Milestone 2 states the corrected perturbation $[x^T\ {-1}]$; the printed $[x^T\ 1]$ is false.
• A trivializing formalization — an upper bound in place of the equality, a worst case over $\Delta A$ and $\Delta b$ bounded separately, or uniqueness among critical points only — is ruled out: the goal is the equality for the jointly bounded augmented matrix and ∃! of a global minimizer over all of $\mathbb{R}^m$.

Contributions welcome: lemmas on Frobenius and operator norms of rank-one matrices, the inequality $\|Mz\| \le \|M\|_F\|z\|$ in this explicit setting, and strict convexity of $x \mapsto \sqrt{\|x\|^2+1}$; these are reusable beyond the mission.

Selected references

• L. El Ghaoui and 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 and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• H. Xu, C. Caramanis and S. Mannor, Robust Regression and Lasso, Journal of Machine Learning Research 10:1485–1510, 2009 (IEEE Trans. Inf. Theory 56(7), 2010). https://jmlr.org/papers/v10/xu09b.html
• M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra and its Applications 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

Motivation

Gradient descent needs a step size, and the classical choices each ask for something the user may not have. A constant step $1/L$ needs the Lipschitz constant $L$ of the gradient, which is rarely known and often pessimistic. Backtracking needs repeated function evaluations. The exact line search needs a one-dimensional minimization at every iteration. Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021, doi:10.1137/20M1329858) proposed a step size for the static linear-quadratic regulator (their rule (4.8), §4.3, p. 11). In §6.1 they point out that the same rule applies to any smooth unconstrained problem $\min_{x\in\mathbb{R}^n} f(x)$. The rule divides the squared gradient norm by the Hessian quadratic form along the gradient. It needs one Hessian–vector product per iteration and neither $L$ nor the strong convexity constant $\mu$. In the paper's LQR experiment (§5, Figure 8, p. 13) the algorithm built on this step converges much faster than gradient descent with a constant step tuned at the first iterations.

The paper proves the method converges linearly for strongly convex functions (Theorem 6.1, p. 13). The proof takes one page (Appendix D.4, p. 19). This mission formalizes that theorem. It is the third mission of a series on this paper; the other two concern the LQR gradient method and gradient flow, and this one uses none of their control-theoretic objects.

Setting

Let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable, with gradient $\nabla f(x)$ and Hessian $\nabla^2 f(x)$. Three constants describe it.

• $f$ is $\mu$-strongly convex, $\mu>0$: $f(ax+by)\le af(x)+bf(y)-ab\,\frac{\mu}{2}\|x-y\|^2$ for all $x,y$ and $a,b\ge0$ with $a+b=1$.
• $\nabla f$ is Lipschitz with constant $L$: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$.
• $\nabla^2 f$ is Lipschitz with constant $M$: $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ in the operator norm.

Let $x_*$ be the global minimizer of $f$. The Hessian step size at a point $x$ is

$$\gamma(x)=\frac{\|\nabla f(x)\|^2}{\langle\nabla^2 f(x)\nabla f(x),\nabla f(x)\rangle},$$

the minimizer of the second-order Taylor model of $f$ along $-\nabla f(x)$. The method (6.1) runs

$$x_{j+1}=x_j-\gamma_j\nabla f(x_j),\qquad\gamma_j=\gamma(x_j),$$

from a starting point $x_0$. The damped method with factor $\sigma>0$ runs $x_{j+1}=x_j-\sigma\gamma_j\nabla f(x_j)$. For a quadratic $f(x)=\langle Hx,x\rangle$ the method (6.1) is steepest descent with exact line search.

Formalization targets

Goal: Theorem 6.1 (p. 13), both parts

Under the hypotheses above:

1. If $\delta>0$ and $M\sqrt{2L(f(x_0)-f(x_*))}\le3\mu^2(1-\delta)$ (condition (6.2)), the iterates of (6.1) satisfy

$$f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\delta}{L}\Bigr)^j\quad\text{for all }j.\tag{6.3}$$

2. If $0<\sigma\le\mu/L$, the damped iterates from any $x_0$ satisfy

$$f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\sigma}{L}\Bigr)^j\quad\text{for all }j.\tag{6.4}$$

The constants are the paper's, stated exactly.

Milestones (Appendix D.4, p. 19)

• Cubic Taylor bound (first display): $\bigl|f(x+y)-f(x)-\langle\nabla f(x),y\rangle-\frac12\langle\nabla^2 f(x)y,y\rangle\bigr|\le\frac M6\|y\|^3$.
• One-step inequality (third display): with $\varphi_j=f(x_j)$, $\varphi_{j+1}\le\varphi_j-\frac12\gamma_j\|\nabla f(x_j)\|^2\bigl(1-\frac{M\gamma_j^2}{3}\|\nabla f(x_j)\|\bigr)$.
• (D.1): $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac{L}{2\mu}\langle\nabla^2 f(x)(y-x),y-x\rangle$.
• (D.2): one damped step gives $f(x_{j+1})\le f(x_j)-\frac{\sigma\gamma_j}{2}\|\nabla f(x_j)\|^2$.

Significance

Theorem 6.1 gives a rate for a step size computed from local second-order information alone. Part 1 says that near the minimizer the method converges at least as fast as gradient descent with step $\delta/L$, with no step-size parameter to tune. Part 2 gives convergence from every starting point, at the price of knowing a lower bound on $\mu/L$ for the damping. The same step appears in the paper's LQR method (rule (4.8)) and in gradient projection methods (p. 13, citing [37]), so the one-step inequalities are reusable beyond this theorem.

The result is proved in the paper. As of this writing none of it has a machine-checked proof. The formal work is the full development: the cubic Taylor bound from a Lipschitz second derivative on $\mathbb{R}^n$, the two one-step inequalities, and the inductions that give the rates.

Difficulty

The obvious argument for gradient descent uses the quadratic upper bound $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac L2\|y-x\|^2$ and a step no larger than $2/L$. The Hessian step can be as large as $1/\mu$, far outside that range, so the quadratic bound in the Euclidean norm gives no decrease. Two different replacements are needed. For the undamped method, the cubic Taylor error must be controlled along the whole trajectory, and condition (6.2) is imposed only on $x_0$: the proof must show the gradient stays small enough at every later iterate. For the damped method, the upper bound must be measured in the local Hessian norm (D.1), which trades the step's size for the condition number $L/\mu$.

On the Lean side, Mathlib has Taylor's theorem in one variable. The cubic bound for a function on $\mathbb{R}^n$ with a Lipschitz Fréchet second derivative must be assembled from it or from the integral form along a segment. Mathlib has no ready-made link between strong convexity and a lower bound on the Hessian either.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient f. The Hessian quadratic form $\langle\nabla^2 f(x)v,v\rangle$ is fderiv ℝ (fderiv ℝ f) x v v. Twice differentiability is differentiability of f and of fderiv ℝ f everywhere. The Lipschitz constant of the Hessian is in the operator norm of the bilinear map, not the Frobenius norm. Strong convexity is StrongConvexOn Set.univ μ f with 0 < μ; Mathlib's modulus is $\frac\mu2\|x-y\|^2$. $L$ and $M$ are real constants in the Lipschitz inequalities. The minimizer $x_*$ is a hypothesis ($f(x_*)\le f(y)$ for all $y$), not constructed.

Deviations from the page, all recorded in the items' Formalization Notes:

• The damping positivity $0<\sigma$ is added. It is implicit on the page.
• The damped claim is stated under the full hypotheses of Theorem 6.1, including the Lipschitz Hessian, although its proof does not use $M$.
• The one-step inequality for (6.1) is stated under the strong convexity of Theorem 6.1, which keeps $\gamma\ge0$. The gradient's Lipschitz constant is not assumed there.

At a stationary point the step is $0/0$; Lean evaluates it to $0$, so the method stays at the minimizer, and both rates remain true.

The iterates are those of the defined recursions (6.1) and its damped version. A statement about an arbitrary sequence satisfying a descent inequality would be a different, weaker theorem and does not discharge the goal. Condition (6.2) is imposed on $x_0$ only; a version assuming it at every iterate is also not the goal.

Contributions welcome: the multivariate cubic Taylor bound (reusable wherever a Lipschitz Hessian appears, e.g. in cubic regularization of Newton's method); the Hessian bounds $\mu I\preceq\nabla^2 f\preceq LI$ from strong convexity and a Lipschitz gradient; and the inequality $\frac12\|\nabla f(x)\|^2\le L(f(x)-f(x_*))$.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, 2020; SIAM J. Control Optim. 59(5), 2021. https://arxiv.org/abs/2004.09875 · https://doi.org/10.1137/20M1329858
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108, 2006 (the cubic Taylor bound for Lipschitz Hessians). https://doi.org/10.1007/s10107-006-0706-8
• B. T. Polyak, Introduction to Optimization, Optimization Software, 1987 (gradient methods, strong convexity).