All missions

Motivation

A convex program whose objective and feasible set are known only through oracles, routines that answer queries about one point at a time, can still be solved to any prescribed accuracy with a number of queries bounded in advance. The ellipsoid method is the classical algorithm that achieves this. It was introduced for convex minimization by Yudin and Nemirovski (Ekonomika i Matematicheskie Metody, 1976) and by Shor (Cybernetics, 1977), and it became widely known when Khachiyan used it to prove that linear programming is solvable in polynomial time (Soviet Math. Dokl., 1979). Grötschel, Lovász and Schrijver turned the method into a general tool of combinatorial optimization, the equivalence of separation and optimization (Springer, 1988).

Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001) present the method in §5.2 as the engine of their theorem that convex programs are polynomially solvable, and prove an explicit, fully quantified complexity bound for it, Theorem 5.2.1. This mission is the tenth of a series formalizing the book's main results and covers §5.2 (pp. 342–352).

Setting

Vectors are elements of $\mathbb R^n$, $n \ge 2$, with the Euclidean norm $\|x\|_2 = \sqrt{x^Tx}$. The problem is

$$\min_x\{f(x) : x \in X \subset \mathbb R^n\} \tag{5.2.9}$$

where $f : \mathbb R^n \to \mathbb R$ is convex and $X$ is a closed, bounded, convex set with nonempty interior. Two radii $r, R > 0$ are known in advance (assumption A): $X$ lies in the ball $E_0 = \{x \mid \|x\|_2 \le R\}$ and contains some ball $\{x \mid \|x - \bar x\|_2 \le r\}$, whose centre $\bar x$ is not known.

The data are accessed through two oracles. A separation oracle for $X$ answers a query $x$ by "$x \in X$" when that holds, and otherwise returns a vector $a \ne 0$ with $a^Tx \ge a^Ty$ for all $y \in X$. A first order oracle for $f$ returns $f(x)$ and a subgradient $\eta$ of $f$ at $x$: $f(y) \ge f(x) + \eta^T(y - x)$ for all $y$.

An ellipsoid is $E(c, B) = \{c + Bu \mid u^Tu \le 1\}$ with $\operatorname{Det} B \ne 0$. For $a \ne 0$, put $p = B^Ta/\sqrt{a^TBB^Ta}$ and

$$c^+ = c - \frac{1}{n+1}Bp,\qquad B^+ = \frac{n}{\sqrt{n^2-1}}B + \Big(\frac{n}{n+1} - \frac{n}{\sqrt{n^2-1}}\Big)(Bp)p^T .$$

The ellipsoid method with accuracy $\epsilon > 0$ starts from $c_0 = 0$, $B_0 = RI$, $L_0 = 0$. At step $t = 1, 2, \dots$ it queries the separation oracle at $c_{t-1}$. If a separator $a$ is returned, the step is nonproductive, $a_t = a$ and $L_t = L_{t-1}$. Otherwise the step is productive: the first order oracle is queried at $c_{t-1}$; a zero subgradient stops the method with result $c_{t-1}$; a nonzero one becomes $a_t$, and $L_t = \max\{L_{t-1}, R\|a_t\|_2 - a_t^Tc_{t-1}\}$. Then $c_t = c_{t-1}^+$, $B_t = B_{t-1}^+$ (computed from $a_t$), $\rho_t = |\operatorname{Det} B_t|^{1/n}$, and the method stops if

$$\frac{\rho_t}{r} < \frac{\epsilon}{L_t + \epsilon}, \tag{5.2.17}$$

returning the productive search point $c_{\tau-1}$, $\tau \le t$, with the smallest value of $f$. Finally $\operatorname{Var}_R(f) = \max_{E_0} f - \min_{E_0} f$.

Formalization targets

Goal: Theorem 5.2.1 (p. 349)

For every accuracy $\epsilon > 0$, every separation oracle for $X$ and every first order oracle for $f$, the ellipsoid method terminates after no more than

$$N(\epsilon) = \operatorname{Ceil}\Big(2n^2\Big[\ln\Big(\frac Rr\Big) + \ln\Big(\frac{\epsilon + \operatorname{Var}_R(f)}{\epsilon}\Big)\Big]\Big) + 1 \tag{5.2.18}$$

steps, and its result $\widehat x$ satisfies

$$\widehat x \in X \quad\text{and}\quad f(\widehat x) - \min_X f \le \epsilon. \tag{5.2.19}$$

Milestones

• Statement (∗), case $n > 1$ (p. 344): the half-ellipsoid $\{x \in E(c,B) \mid a^Tx \le a^Tc\}$ lies in $E(c^+, B^+)$, and $\operatorname{Vol}E(c^+,B^+) = (n/\sqrt{n^2-1})^{n-1}\frac{n}{n+1}\operatorname{Vol}E(c,B) \le e^{-1/(2n)}\operatorname{Vol}E(c,B)$.
• Eq. (5.2.21) (p. 350): $\rho_\tau \le e^{-\tau/(2n^2)}R$ at every step performed.
• Eq. (5.2.28) (p. 352): $L_t \le \operatorname{Var}_R(f)$ for every $t$.
• Claim 2∗ (p. 350): whenever the method terminates, its result is well defined and is a feasible $\epsilon$-solution.

Significance

Theorem 5.2.1 bounds the number of oracle calls by a quantity that depends only on the dimension, on $\ln(R/r)$ and on $\ln(1 + \operatorname{Var}_R(f)/\epsilon)$: the cost of each additional digit of accuracy is $O(n^2)$ steps, whatever the instance. Each step costs one call of each oracle and $O(n^2)$ arithmetic operations. This is the ingredient the book's Theorem 5.3.1 combines with polynomial computability to conclude that convex programs are polynomially solvable, and it is the reason semidefinite and conic quadratic programs, the subject of the earlier lectures, are tractable in theory. The bound is also explicit enough to be checked numerically, with no hidden constants.

On the formal side, the platform has machine-checked versions of related results in other forms: Bertsimas and Tsitsiklis's half-ellipsoid lemma with the weaker ratio $e^{-1/(2(n+1))}$ and polyhedral feasibility version, Bubeck's version for objectives bounded on $X$ with a convergence-rate conclusion, and Shor's localization theorem. None of these is the book's method: its guesses $L_t$, its stopping rule (5.2.17), the explicit step count (5.2.18), or the exact volume identity (5.2.14). A formal proof of Theorem 5.2.1 gives a machine-checked oracle complexity bound with a stopping rule computable from the run alone.

Difficulty

The book's description of the method runs to two pages; the central difficulty is the termination analysis, not the geometry. The volume of the ellipsoids decreases geometrically, but their diameters need not, so the search points $c_t$ need not converge, and the method cannot know how close it is to the optimum. A naive argument that the search points approach the optimum therefore fails, and the stopping test (5.2.17), which only sees $\rho_t$, $r$ and the guesses $L_t$, has to be related to the unknown optimality gap. The analysis must also cover runs in which no step was productive for a long time, and the possibility that the result is undefined. On the geometric side, (∗) requires the exact determinant of a rank-one update and the elementary but not immediate inequality $(n/\sqrt{n^2-1})^{n-1}\frac{n}{n+1} \le e^{-1/(2n)}$. Reasoning about a recursively defined algorithm also means carrying invariants (the ellipsoid contains every point of $X$ not yet cut off, $\operatorname{Det} B_t \ne 0$) through the induction.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and the Euclidean norm eucNorm x = √(x ⬝ᵥ x) is defined explicitly (Mathlib's norm on Fin n → ℝ is the sup norm). Volumes are MeasureTheory.volume on Fin n → ℝ, valued in ℝ≥0∞. The setting (5.2.9) with assumption A is the predicate IsBlackBoxProgram f X r R. The oracles are arbitrary functions of the query point satisfying (5.2.10) and (5.2.11); every theorem is quantified over all of them, and none sees the centre $\bar x$. The method is a function run from the number of steps performed to an outcome, running with the current $c_t, B_t, L_t$ and best productive point, or stopped with an optional result; TerminatesAt t res says the run stops exactly at step $t \ge 1$. $\max_{E_0} f$ and $\min_{E_0} f$ are reals given by IsGreatest/IsLeast, and $\min_X f$ is expressed by comparison with every point of $X$, so no supremum or infimum with a default value occurs. Ceil is Int.ceil and the step bound is compared in $\mathbb Z$. A statement about an arbitrary sequence of ellipsoids or an arbitrary "state" carrying no link to the run would trivialize the goal; here the ellipsoids, guesses and result are those the method constructs from the oracles' answers.

Beyond the paper. The book's statement (∗) also has a case $n = 1$, whose printed centre $c - \frac12 Ba/|Ba|$ moves by $\frac12$ regardless of the segment's length; the containment fails for $c = 0$, $B = 4$, $a = 1$. The case is posed as printed (expected to be disproved) and as a corrected variant with centre $c - \frac12 B\,(Ba/|Ba|)$. Theorem 5.2.1 assumes $n \ge 2$ and is unaffected.

A complete development needs the determinant of a rank-one update (Matrix.det_add_replicateCol_mul_replicateRow), Lebesgue measure of linear images (MeasureTheory.Measure.addHaar_image_linearMap), the continuity of convex functions on $\mathbb R^n$, and an induction over run. The ellipsoid update lemma and the oracle and method definitions are reusable for other cutting-plane methods. Proofs of individual milestones, in particular (∗), are welcome as separate contributions.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, MPS/SIAM Series on Optimization, SIAM, 2001. doi:10.1137/1.9780898718829
• D. B. Yudin, A. S. Nemirovski, Informational complexity and efficient methods for the solution of convex extremal problems, Ekonomika i Matematicheskie Metody 12 (1976), 357–369.
• N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13 (1977), 94–96. doi:10.1007/BF01071394
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Math. Doklady 20 (1979), 191–194. mathnet
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. doi:10.1007/978-3-642-97881-4

Motivation

Semidefinite programming (SDP), the optimization of a linear function over the intersection of an affine subspace with the cone of positive semidefinite matrices, is the workhorse behind relaxations in combinatorial optimization, robust optimization and control. Its practical and theoretical tractability rests on interior point methods: algorithms that follow the central path, a curve of strictly feasible primal-dual pairs parametrized by a penalty parameter $t > 0$, along which the duality gap equals $k/t$. The polynomial-time analysis of these methods, due to Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994) and, for the primal-dual SDP family considered here, to Monteiro and Zhang and others in the 1990s, reduces to one local statement: a single Newton-type update, started close to the path, lands close to the path again while the penalty parameter grows by a factor $1 + \Omega(k^{-1/2})$.

This mission formalizes that local statement in the form given by Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM 2001), Lecture 6, Theorem 6.5.2, for the whole family of primal-dual updates obtained from commutative scalings.

Setting

Let $k \ge 1$ and let $\mathbf S^k$ be the space of real symmetric $k\times k$ matrices with the Frobenius inner product $\langle X, Y\rangle_F = \operatorname{Tr}(XY)$ and norm $\|A\|_2 = \sqrt{\sum_{i,j}A_{ij}^2}$. For $X \succeq 0$, $X^{1/2}$ is its positive semidefinite square root. Fix a linear subspace $\mathcal L \subseteq \mathbf S^k$, its orthogonal complement $\mathcal L^\perp$ in $\mathbf S^k$, and $B, C \in \mathbf S^k$. The primal-dual pair is

$$\text{(P)}\ \min_X\{\operatorname{Tr}(CX) : X \in (\mathcal L - B)\cap\mathbf S^k_+\},\qquad \text{(D)}\ \max_S\{\operatorname{Tr}(BS) : S \in (\mathcal L^\perp + C)\cap\mathbf S^k_+\}.$$

$X$ is strictly primal feasible if $X \in \mathcal L - B$ and $X \succ 0$; $S$ is strictly dual feasible if $S \in \mathcal L^\perp + C$ and $S \succ 0$. For such a pair the duality gap is $\operatorname{Tr}(CX) - \operatorname{Tr}(BS) + \operatorname{Tr}(CB) = \operatorname{Tr}(XS)$.

The distance of a pair $X, S \succ 0$ to the point of the central path with parameter $t$ is

$$\operatorname{dist}((X,S), Z_*(t)) = \|tX^{1/2}SX^{1/2} - I\|_2 ,$$

and the neighbourhood $\mathcal N_\kappa$ consists of the triples $(t, X, S)$ with $t > 0$, $X, S$ strictly feasible and distance at most $\kappa$.

The updating (U), with parameters $\kappa, \chi$, takes a strictly feasible pair $(\bar X, \bar S)$ and

1. sets $\bar t = k/\operatorname{Tr}(\bar X\bar S)$ and $t_+ = (1 - \chi/\sqrt k)^{-1}\,\bar t$;
2. takes any $Q \succ 0$ such that $Q\bar XQ$ and $Q^{-1}\bar SQ^{-1}$ commute;
3. solves, for symmetric $\Delta X \in \mathcal L$, $\Delta S \in \mathcal L^\perp$, the linear system

$$Q[\Delta X\,\bar S + \bar X\,\Delta S]Q^{-1} + Q^{-1}[\Delta S\,\bar X + \bar S\,\Delta X]Q = \tfrac{2}{t_+}I - [Q\bar X\bar SQ^{-1} + Q^{-1}\bar S\bar XQ];$$

4. returns $X_+ = \bar X + \Delta X$, $S_+ = \bar S + \Delta S$.

The choices $Q = \bar X^{-1/2}$, $Q = \bar S^{1/2}$ and the Nesterov–Todd scaling are all admissible in step 2.

Formalization targets

Goal: Theorem 6.5.2

If $0 < \chi \le \kappa \le 0.1$ and the strictly feasible pair $(\bar X, \bar S)$ satisfies $\|\bar t\,\bar X^{1/2}\bar S\bar X^{1/2} - I\|_2 \le \kappa$, then for every admissible $Q$ the system of step 3 has exactly one solution, and

$$X_+ \text{ and } S_+ \text{ are strictly feasible},\qquad t_+ = \frac{k}{\operatorname{Tr}(X_+S_+)},\qquad (t_+, X_+, S_+) \in \mathcal N_\kappa .$$

Milestones

The proof reduces to the case $Q = I$ with $\bar X = \operatorname{Diag}(x)$, $\bar S = \operatorname{Diag}(s)$ and $\operatorname{Tr}(\bar X\bar S) = k$, and the milestones are the numbered facts of that reduced situation, with $\mu_+ = 1 - \chi k^{-1/2}$ and $\rho = \sqrt{\chi^2+\kappa^2}/(1-\kappa)$:

• (6.4.11): $\operatorname{Tr}(X(tS - X^{-1})X(tS - X^{-1})) = \|tX^{1/2}SX^{1/2} - I\|_2^2$.
• Proposition 6.4.2, SDP case: $\operatorname{dist} \le 1$ implies $\operatorname{Tr}(XS) \le 2k/t$.
• Step 3∗: the reduced system $\Delta X\cdot S + X\cdot\Delta S + \Delta S\cdot X + S\cdot\Delta X = 2\mu_+I - 2XS$, $\Delta X \in \mathcal L$, $\Delta S \in \mathcal L^\perp$ has a unique solution.
• (6.5.64)–(6.5.65): $\|X^{-1/2}\Delta XX^{-1/2}\|_2 \le \rho$ and $\|X^{1/2}\Delta SX^{1/2}\|_2 \le (1+\kappa)\rho$.
• 2∗(i)–(ii), (6.5.47), (6.5.66): $X_+, S_+$ are strictly feasible, $\operatorname{Tr}(X_+S_+) = \mu_+k$, $X_+ \preceq (1+\rho)X$.
• (6.5.73): $\|\mu_+^{-1}X_+^{1/2}S_+X_+^{1/2} - I\|_2 \le \frac{\rho(1+\rho)}{1-\chi k^{-1/2}}\big[\frac{\chi}{\sqrt k} + \frac{\rho}{1-\rho} + \frac{\kappa}{1-\kappa}\big]$.
• p. 421: for $0 < \chi \le \kappa \le 0.1$ and every $k \ge 1$ the right-hand side of (6.5.73) is at most $\kappa$.

Significance

Theorem 6.5.2 is the step that turns the central path into an algorithm: once a pair in $\mathcal N_{0.1}$ is known, iterating (U) keeps every iterate in $\mathcal N_{0.1}$ and increases the penalty parameter by a constant factor every $O(\sqrt k)$ steps, so the duality gap $\operatorname{Tr}(XS) \le 2k/t$ (Proposition 6.4.2) falls below $\epsilon$ after $O(\sqrt k\ln(1/\epsilon))$ steps. The statement covers a whole family of search directions at once, including the Nesterov–Todd direction used by SDP solvers, and by Remark 6.5.2 it specializes to LP when all matrices are diagonal.

The result is classical and proved in the book; it has not been machine-checked. The platform has formalizations of central-path facts for LP and for inequality-form barrier problems, and open items on self-scaled short-step methods, but no statement about primal-dual Newton steps for SDP. A formal proof would supply reusable matrix-analysis infrastructure: Frobenius estimates through eigenvalues, the Löwner order under congruence, and unique solvability of Sylvester-type systems with subspace constraints.

Difficulty

The obvious approach, perturbation analysis of the Newton system in the original variables, does not close: the bound has to hold uniformly in the condition of $\bar X$ and $\bar S$, and only the scaled quantities $\delta X = X^{-1/2}\Delta XX^{-1/2}$, $\delta S = X^{1/2}\Delta SX^{1/2}$ are controlled by $\kappa$ and $\chi$. The reduction to $Q = I$ with diagonal commuting $\bar X, \bar S$ has to be justified, including invariance of the distance under scaling and the change of the subspaces $\mathcal L$, $\mathcal L^\perp$ to $Q\mathcal LQ$, $Q^{-1}\mathcal L^\perp Q^{-1}$. Uniqueness uses the orthogonality $\operatorname{Tr}(\Delta X\Delta S) = 0$ in an essential way. The final estimate passes from the scaled distance to the distance measured at the new point $X_+$, which needs the Löwner bound $X_+ \preceq (1+\rho)X$ and monotonicity of the trace under congruence. The concluding numerical inequality holds for every $k \ge 1$, not only asymptotically.

Formalization scope

All matrices are Matrix (Fin k) (Fin k) ℝ with $k \ge 1$. $\mathcal L$ is a Submodule ℝ of matrices with every element symmetric, and $\mathcal L^\perp$ is the set of symmetric $S$ with $\operatorname{Tr}(XS) = 0$ for all $X \in \mathcal L$, so the unknowns of the linear systems are symmetric. $X^{1/2}$ is Mathlib's CFC.sqrt (with open scoped MatrixOrder), positive (semi)definiteness is Matrix.PosDef/Matrix.PosSemidef, and the Frobenius norm is defined explicitly. The book's (P) comes from a conic problem $\min\{c^Tx : \mathcal Ax - B \succeq 0\}$ under Assumption A ($\mathcal A$ injective) with $\mathcal L = \operatorname{Im}\mathcal A$; every subspace is such an image, so the formal statements quantify over subspaces. The distance to the central path is defined by its SDP closed form (6.4.11), so no existence result for the central path is needed. The goal is stated for every admissible scaling $Q$, and "the system has a unique solution" is a separate conjunct from the properties of that solution, so the goal cannot hold vacuously through an unsolvable system. The milestones of the proof are stated in the book's reduced situation (diagonal $\bar X, \bar S$, $Q = I$, $\operatorname{Tr}(\bar X\bar S) = k$) with all of its hypotheses.

Results of §§6.3–6.4 for general canonical cones (products of semidefinite and Lorentz cones with their barriers $-\ln\operatorname{Det}X$ and $-\ln(x^TJx)$), namely Propositions 6.3.1–6.3.2 and Theorems 6.4.1–6.4.2, and Theorem 6.5.1 (primal path-following), are not part of this mission: they need a calculus of canonical barriers on block-structured spaces. Proofs of any milestone, reusable lemmas on the Löwner order and the matrix square root, and a sorry-free proof of the numerical inequality are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, MPS/SIAM Series on Optimization, SIAM, 2001, Lecture 6, §§6.4–6.5. https://doi.org/10.1137/1.9780898718829
• Yu. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• Y. Zhang, On extending some primal–dual interior-point algorithms from linear programming to semidefinite programming, SIAM Journal on Optimization 8(2), 1998, 365–386. https://doi.org/10.1137/S1052623495296115
• R. D. C. Monteiro, Primal–dual path-following algorithms for semidefinite programming, SIAM Journal on Optimization 7(3), 1997, 663–678. https://doi.org/10.1137/S1052623495293056
• Yu. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1), 1997, 1–42. https://doi.org/10.1287/moor.22.1.1

Motivation

Many questions in robust control and robust optimization reduce to one test: does a whole family of symmetric matrices, generated by perturbing a nominal matrix along several directions at once, stay positive semidefinite? A linear system whose coefficients are only known to lie in intervals is a typical case. Showing that one quadratic Lyapunov function certifies stability of every member of such an interval matrix comes down to exactly this test. Ben-Tal and Nemirovski isolate it as the Matrix Cube problem. The problem is NP-hard (Ben-Tal & Nemirovski, On tractable approximations of uncertain linear matrix inequalities affected by interval uncertainty, SIAM J. Optim. 12 (2002)). They prove that a simple semidefinite sufficient condition is never far from exact. The gap is controlled by a universal factor that depends only on the ranks of the perturbation directions.

This mission formalizes that result as it appears in §4.4.3 of Lectures on Modern Convex Optimization (Ben-Tal & Nemirovski, SIAM 2001), pp. 189–197, together with the lemmas its proof uses and its application to interval Lyapunov stability.

Setting

Matrices are real. $\mathbf S^n$ is the space of symmetric $n\times n$ matrices, $\mathbf S^n_+$ its positive semidefinite cone, and $X\succeq Y$ means $X-Y\in\mathbf S^n_+$. For $X\in\mathbf S^n$, $\lambda(X)$ is its vector of eigenvalues, so $\|\lambda(X)\|_1$ is the sum of their absolute values.

Fix $A_0,A_1,\dots,A_m\in\mathbf S^n$ with $A_0\succeq0$. For a level $\rho\ge0$ the matrix cube is

$$\mathcal A_\rho=\Big\{A_0+\sum_{i=1}^m z_iA_i \;:\; \|z\|_\infty\le\rho\Big\},$$

the image of the cube $\{\|z\|_\infty\le\rho\}$ under an affine map. The Matrix Cube problem asks for the largest $\rho=R[A_1,\dots,A_m:A_0]$ with $\mathcal A_\rho\subset\mathbf S^n_+$.

The system of LMIs $(S_\rho)$ in symmetric variables $X^1,\dots,X^m$ is

$$X^i\succeq\rho A_i,\quad X^i\succeq-\rho A_i\ (i=1,\dots,m),\qquad \sum_{i=1}^mX^i\preceq A_0 .$$

Its feasibility can be checked by semidefinite programming. The largest $\rho$ for which it is solvable is $\rho[A_1,\dots,A_m:A_0]$, the optimal value of the semidefinite problem (4.4.45).

The approximation factor is the function

$$\theta(k)=\frac{1}{\min\Big\{\int_{\mathbb R^k}|\alpha_1u_1^2+\cdots+\alpha_ku_k^2|\,p_k(u)\,du \;:\; \alpha\in\mathbb R^k,\ \|\alpha\|_1=1\Big\}},\qquad k\ge1,$$

where $p_k(u)=(2\pi)^{-k/2}\exp\{-u^Tu/2\}$ is the standard Gaussian density on $\mathbb R^k$. The relevant rank is $\mu=\max_{1\le i\le m}\operatorname{Rank}(A_i)$; $A_0$ is not included.

For the application, $A^*$ is a stable $n\times n$ matrix (all eigenvalues in the open left half-plane). $D\neq0$ has nonnegative entries, and $\mathcal U_\rho=\{A:|A_{ij}-A^*_{ij}|\le\rho D_{ij}\}$ is the interval matrix. $(\mathrm{Ly}[\rho])$ asks for $X\succeq I$ with $A^TX+XA\preceq-I$ for all $A\in\mathcal U_\rho$, and $R[A^*,D]$ is the supremum of the $\rho\ge0$ for which it is solvable. $(\mathrm A[\rho])$ is the analogue of $(S_\rho)$ for this cube. It uses matrix variables $X$ and $X^{ij}$ for $(i,j)\in\mathcal D=\{D_{ij}>0\}$, and $\rho[A^*,D]$ is its supremum.

Formalization targets

Goal: the Matrix Cube Theorem (Theorem 4.4.1)

For all $n,m$, all $A_0\succeq0$, all $A_1,\dots,A_m\in\mathbf S^n$ and all $\rho\ge0$:

$$(S_\rho)\ \text{not solvable}\ \Longrightarrow\ \mathcal A_{\theta(\mu)\rho}\not\subset\mathbf S^n_+ ,$$

and

$$\theta(k)\le\frac{\pi\sqrt k}{2}\ \ (k\ge1),\qquad \theta(2)=\frac{\pi}{2}.$$

Milestones, in attack order

1. Proposition 4.4.5. If $(S_\rho)$ is solvable then $\mathcal A_\rho\subset\mathbf S^n_+$.
2. Lemma 4.4.3. For $W\succeq0$ and $A\in\mathbf S^n$,

$$\max_{U,V\succeq0,\,U+V=W}\operatorname{Tr}([U-V]A)=\max_{X=X^T,\ \|\lambda(X)\|_\infty\le1}\operatorname{Tr}(XW^{1/2}AW^{1/2})=\|\lambda(W^{1/2}AW^{1/2})\|_1 .$$

3. Lemma 4.4.4. For $\xi\sim\mathcal N(0,I_n)$ and $A\in\mathbf S^n$: $\mathbf E\{\xi^TA\xi\}=\operatorname{Tr}(A)$ and $\mathbf E\{|\xi^TA\xi|\}\ge\|\lambda(A)\|_1/\theta(\operatorname{Rank}(A))$.
4. Eq. (4.4.37). $\theta(k)\le\pi\sqrt k/2$ for $k\ge1$, and $\theta(2)=\pi/2$.
5. Corollary 4.4.1. If all $\operatorname{Rank}(A_i)\le\mu$, then

$$\rho[A_1,\dots,A_m:A_0]\le R[A_1,\dots,A_m:A_0]\le\theta(\mu)\,\rho[A_1,\dots,A_m:A_0].$$

6. Proposition 4.4.6. If $(\mathrm A[\rho])$ is solvable, its $X$-component solves $(\mathrm{Ly}[\rho])$. If it is not solvable, neither is $(\mathrm{Ly}[\pi\rho/2])$. Hence $\rho[A^*,D]\le R[A^*,D]\le\frac\pi2\rho[A^*,D]$.
7. Lemma 4.4.5. $\|\lambda(fg^T+gf^T)\|_1=2\|f\|_2\|g\|_2$.

Significance

The result. Proposition 4.4.5 and Theorem 4.4.1 together bound the cube radius. It lies between the efficiently computable $\rho[\cdot]$ and $\theta(\mu)\rho[\cdot]$. The factor is $\pi\sqrt\mu/2$ in general, independent of $n$ and $m$, and exactly $\pi/2$ when every perturbation has rank at most two. Rank two is the situation of interval matrices, of Lyapunov certificates for interval systems (Proposition 4.4.6), and of a re-derivation of Nesterov's $\pi/2$ theorem for quadratic maximization over the unit cube (pp. 200–201). The same estimate underlies tractable approximations of robust LMIs with box uncertainty in robust semidefinite optimization.

Formalizing it. The results are proved in the book. None of them, and nothing on the matrix cube, the function $\theta$ or interval Lyapunov stability, is machine-checked on the platform. The formalization adds three things: a checked definition of $\theta$ as a Gaussian integral; a checked proof of the constants $\pi\sqrt k/2$ and $\pi/2$; and a checked bridge from semidefinite duality to a probabilistic rounding argument. The proof of Proposition 4.4.5 already has a sorry-free local check, which also exposed a sign slip in the printed proof.

Difficulty

The sufficient direction is elementary. The converse is not. Unsolvability of $(S_\rho)$ is a statement about a semidefinite program, and turning it into an explicit point $z$ with $\|z\|_\infty\le\theta(\mu)\rho$ and $A_0+\sum z_iA_i\not\succeq0$ needs three ingredients:

• a strictly feasible conic duality argument, to obtain dual certificates;
• an exact spectral identity (Lemma 4.4.3);
• an averaging argument over a Gaussian direction, with a sharp lower bound on $\mathbf E|\xi^TA\xi|$ in terms of rank and trace norm.

Bounding coordinate by coordinate, or using a worst-case vertex of the cube, gives a factor that grows with $m$. The rank-dependent constant is what makes the theorem useful.

The constants need real analysis on Gaussian integrals. $\theta(2)=\pi/2$ requires an exact minimization of $\int|\theta u_1^2-(1-\theta)u_2^2|p_2(u)\,du$ over $\theta\in[0,1]$. The bound $\pi\sqrt k/2$ requires a symmetrization and an independence argument. Lemma 4.4.4 needs rotational invariance of the Gaussian measure and diagonalization inside an integral.

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℝ, and $X\succeq Y$ is (X - Y).PosSemidef (which includes symmetry). The index $i=1,\dots,m$ is Fin m, and $\|z\|_\infty\le\rho$ is $|z_i|\le\rho$ for every $i$.
• $W^{1/2}$ is CFC.sqrt W under MatrixOrder. Eigenvalues are Mathlib's IsHermitian.eigenvalues, used only through order-independent quantities.
• Expectations under $\mathcal N(0,I_n)$ are Lebesgue integrals against the density $p_n$, which is how the book describes the distribution.
• $\theta$ is the specific function (4.4.38), with the minimum as a real infimum, attained for $k\ge1$. The book leaves $\theta(0)$ undefined. Lean's formula gives it the value $0$, and no statement depends on it: where $\mu=0$ the hypotheses of Theorem 4.4.1 cannot hold, and Corollary 4.4.1 assumes $\mu\ge1$.
• The radii $R[\cdot]$, $\rho[\cdot]$, $R[A^*,D]$, $\rho[A^*,D]$ are suprema in EReal, so $+\infty$ is represented. Ratios are stated in product form, for example $R\le\theta(\mu)\rho[\cdot]$. The "max" in (4.4.45) is stated as attained.
• The level $\rho\ge0$ is a hypothesis, as in the book's setting. For negative $\rho$ the cube is empty and the theorem fails.

A formalization that replaced $\theta$ by an arbitrary function satisfying (4.4.37), or set $\mu=\max_{0\le i\le m}$, or allowed $\rho<0$, would state a different (false or ill-posed) theorem; the statements here rule these out.

Infrastructure needed and reusable beyond this mission:

• Gaussian integrals of quadratic forms on $\mathbb R^n$ and their rotation invariance;
• the trace-norm identity of Lemma 4.4.3;
• strict-feasibility semidefinite duality for the problem (4.4.39);
• the spectrum of rank-two symmetric matrices.

Contributions of separate lemmas are welcome, for example monotonicity of $\theta$ or $\theta(1)=1$.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM/MPS Series on Optimization, 2001, §4.4.3. https://doi.org/10.1137/1.9780898718829
• A. Ben-Tal, A. Nemirovski, On tractable approximations of uncertain linear matrix inequalities affected by interval uncertainty, SIAM Journal on Optimization 12(3), 2002. https://doi.org/10.1137/S1052623401384392
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optimization Methods and Software 9, 1998. https://doi.org/10.1080/10556789808805690

Motivation

A homogeneous quadratic inequality $x^TBx \ge 0$ may hold at every point where other quadratic inequalities $x^TA_ix \ge 0$ hold. Deciding when this happens is the quadratic analogue of the question the Farkas lemma answers for linear inequalities. It is the core of robust optimization with ellipsoidal uncertainty, of absolute stability in control (where it is known as the S-procedure), and of trust-region and quadratically constrained programming. The answer one wants is a linear certificate: nonnegative multipliers $\lambda_i$ with $B \succeq \sum_i \lambda_iA_i$, a condition that can be checked by semidefinite programming.

Lecture 4 of Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), states the classical case and, in its exercises (§4.10.5), traces how far it extends:

• V. A. Yakubovich (1971) proved the S-lemma: with one strictly feasible constraint, the certificate exists exactly when the implication holds.
• L. L. Dines (1941) proved that the joint range $\{(x^TAx, x^TBx)\}$ of two quadratic forms is convex.
• B. T. Polyak (J. Optim. Theory Appl. 99, 1998, doi:10.1023/A:1021798932766) proved that for $n \ge 3$ the joint range of three forms is closed and convex once some linear combination of the matrices is positive definite. From this he derived an S-lemma with two constraints.
• For three constraints, or without Polyak's hypotheses, the certificate can fail to exist even though the implication holds (Exercises 4.47, 4.54, 4.56 of the book).

Setting

Vectors are $x \in \mathbb R^n$ and matrices are real $n\times n$. For a symmetric matrix $A$, the quadratic form is $x^TAx$. $P \succeq Q$ means that $P - Q$ is positive semidefinite, and $P \succ 0$ means $P$ is positive definite. A quadratic inequality $x^TCx \ge 0$ is a consequence of a system $x^TAx \ge 0$, $x^TBx \ge 0$ if it holds at every $x \in \mathbb R^n$ satisfying the system. The system is strictly feasible if some $\bar x$ satisfies both inequalities strictly.

The inhomogeneous case uses $f(x) = x^TAx + 2a^Tx + \alpha$ and $g(x) = x^TBx + 2b^Tx + \beta$. For the topological steps, $S^{n-1}$ is the unit sphere of $\mathbb R^n$. The projective space $P^{n-1}$ is $S^{n-1}$ with each $e$ identified with $-e$, and $\Phi : S^{n-1} \to P^{n-1}$ is the canonical projection.

Formalization targets

Goal: the two-constraint S-lemma, (SL.C) (pp. 306–307)

Let $n \ge 3$ and let $A, B, C$ be symmetric matrices such that (i) some linear combination $aA + bB + cC$ is positive definite and (ii) $\bar x^TA\bar x > 0$, $\bar x^TB\bar x > 0$ for some $\bar x$. Then

$$\Big(\forall x:\ x^TAx \ge 0,\ x^TBx \ge 0 \Rightarrow x^TCx \ge 0\Big) \iff \exists\, \lambda, \mu \ge 0:\ C \succeq \lambda A + \mu B.$$

Milestones

1. Proposition 4.3.4 (p. 176): if $B \succeq \sum_i\lambda_iA_i$ with $\lambda_i \ge 0$, then $x^TA_ix \ge 0$ for all $i$ implies $x^TBx \ge 0$.
2. Theorem 4.3.3, S-lemma (p. 176): if $\bar x^TA\bar x > 0$ for some $\bar x$, then $x^TBx \ge 0$ is a consequence of $x^TAx \ge 0$ iff $B \succeq \lambda A$ for some $\lambda \ge 0$.
3. Proposition 4.10.1, inhomogeneous S-lemma (p. 303): if $f(\bar x) < 0$ for some $\bar x$, then $f \le 0 \Rightarrow g \le 0$ holds iff $g \le \lambda f$ on $\mathbb R^n$ for some $\lambda \ge 0$. Equivalently, as printed, iff $\begin{pmatrix}\lambda\alpha & [\lambda a - b]^T\\ \lambda a - b & \lambda A - B\end{pmatrix} \succeq 0$ for some $\lambda \ge 0$. If moreover $g(x) \ge 0$ is strictly feasible, then $\lambda > 0$.
4. Theorem 4.10.1, general Helly theorem (p. 305): a family of closed convex sets in $\mathbb R^n$ has a common point if every $n+1$ of them do and some finite subfamily has bounded intersection.
5. (SL.B) (p. 305): if $\bar x^TA\bar x > 0$ for some $\bar x$ and $x^TAx \ge 0$, $x \ne 0$ imply $x^TBx > 0$, then $B \succeq \lambda A$ for some $\lambda \ge 0$.
6. Proposition 4.10.2 (p. 308): if any two points of $Y \subset S^{n-1}$ can be linked inside $Y$ to a common antipodal pair $\{y, -y\}$, then $\Phi(Y)$ is path connected.
7. Proposition 4.10.4 (p. 308): for $n \ge 3$ and a nonempty zero set $Y = \{x \in S^{n-1} : x^TQx = 0\}$, $Y = -Y$ and $\Phi(Y)$ is connected.
8. (SL.D), Polyak's theorem (p. 307): for $n \ge 3$ and symmetric $A_1, A_2, A_3$ with a positive definite linear combination, $\{(x^TA_1x, x^TA_2x, x^TA_3x) : x \in \mathbb R^n\}$ is closed and convex.

Significance

The S-lemma converts a semi-infinite family of quadratic implications into one linear matrix inequality. This is what makes robust counterparts of conic quadratic constraints with ellipsoidal uncertainty semidefinite-representable (Proposition 4.5.1 of the book), and it gives trust-region subproblems and quadratic programs with one constraint their exact semidefinite duals. The two-constraint version extends this exactness to problems with two quadratic constraints in dimension at least three. Polyak's convexity theorem is the structural fact behind it, and it is of independent use in the study of joint numerical ranges.

All statements are proved in the literature. On Prove2Me, the inhomogeneous S-procedure in another sign convention is proved (ConvexOptimization.s_procedure), as is the finite Helly theorem (FamousTheorems.helly_theorem). The homogeneous S-lemma is a special case of the former but is not stated on the platform. The infinite Helly theorem with the boundedness condition, Polyak's theorem, the projective-space connectedness facts and the two-constraint S-lemma have no machine-checked statement or proof there. Two statements beyond the book are posed alongside it (see Formalization scope).

Difficulty

The "if" directions are one line each. Every "only if" direction must produce multipliers from a pointwise implication, and there is no Farkas lemma for quadratic inequalities to do it. With two constraints a direct separation argument needs the joint range of three quadratic forms to be convex. That range is not convex in general, and it can fail to be convex for $n = 2$, so any argument has to use the dimension. The book's milestones for this step are topological: paths on spheres, quotients by the antipodal map, and connectedness in projective space. None of this is packaged for this use in Mathlib. Two printed details mislead a solver who follows the page. The matrix in Proposition 4.10.1 omits $-\beta$ in its northwestern entry. The hint for (SL.C) (Exercise 4.48) asks for a positive definite combination $\theta C - \lambda A - \mu B$, where only semidefiniteness can be obtained. The proof of Theorem 4.3.3 also swaps the roles of $D^TAD$ and $D^TBD$ at one step.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The form $x^TAx$ is x ⬝ᵥ (A *ᵥ x) and symmetry is Matrix.IsHermitian. $\succeq 0$ and $\succ 0$ are Mathlib's Matrix.PosSemidef and Matrix.PosDef, both of which include symmetry. The bordered $(n+1)\times(n+1)$ matrix of Proposition 4.10.1 is indexed by Unit ⊕ Fin n with the scalar entry first, as printed. For Propositions 4.10.2 and 4.10.4, the sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1. $P^{n-1}$ is its quotient by $e \sim \pm e$ with the quotient topology (one definition item), which has the same topology as the book's metric $\min\{\|e+e'\|_2, \|e-e'\|_2\}$. The book's linear connectedness, which allows the empty set, is stated pairwise. Every hypothesis of the page is an explicit binder. In particular, strict feasibility appears in every S-lemma variant, $n \ge 3$ appears in (SL.C), (SL.D) and Proposition 4.10.4, and the positive definite combination in (SL.C) involves all three of $A, B, C$ with coefficients of any sign. The implication is quantified over all of $\mathbb R^n$ and the multipliers carry their sign constraints. Dropping (ii), or leaving $\lambda, \mu$ unconstrained, turns the goal into a statement that is false or trivial, and neither is the book's.

Beyond the paper. Two variants are posed beside the faithful items. One is a corrected Proposition 4.10.1 with northwestern entry $\lambda\alpha - \beta$: as printed, the matrix criterion fails for $n = 1$, $f = x^2 - 1$, $g = x^2 - 4$. The other is a sharpness probe of (SL.C) without $n \ge 3$, for which $A = \mathrm{diag}(1,-1)$, $B = \begin{pmatrix}0&1\\1&0\end{pmatrix}$, $C = \begin{pmatrix}0&1\\1&-2\end{pmatrix}$ is a counterexample; its disproof is the sought outcome.

Contributions welcome: the joint range of quadratic forms (Dines's theorem, Polyak's theorem), the projective space as a topological space, and infinite Helly-type intersection theorems. All are reusable beyond this chapter.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. doi:10.1137/1.9780898718829
• B. T. Polyak, Convexity of quadratic transformations and its use in control and optimization, J. Optim. Theory Appl. 99 (1998), 553–583. doi:10.1023/A:1021798932766
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007), 371–418. doi:10.1137/S003614450444614X
• L. L. Dines, On the mapping of quadratic forms, Bull. Amer. Math. Soc. 47 (1941), 494–498. doi:10.1090/S0002-9904-1941-07494-X

Motivation

Truss topology design asks for the stiffest elastic bar construction that can be built from a given set of potential bars with a given amount of material. It is one of the oldest test cases of structural optimization (Bendsøe and Sigmund, Topology Optimization, Springer 2003) and one of the main applications in Ben-Tal and Nemirovski's Lectures on Modern Convex Optimization (SIAM 2001). The quantity being minimized, the compliance of the truss under a load, is defined through the solution of a linear system and takes the value $+\infty$ when the structure cannot carry the load, so it is not obviously a convex function, let alone one a solver can handle. Lecture 1 of the book shows that the single-load problem happens to become a linear program. Section 3.4.3 explains why: the compliance, as a function of the bar volumes and of the load jointly, is conic quadratic representable, and its epigraph has an explicit description by second-order cone constraints. That description is what turns multiload designs, bounds on bar volumes and other variants into conic quadratic programs.

This mission is the fourth of a series formalizing the book's main results, and covers Lecture 3, §3.4.3 (pp. 120–128), together with Proposition 2.4.2 of Lecture 2, on which it relies.

Setting

A ground structure $(n, m, B_1, \dots, B_n)$ consists of real $m \times k_i$ matrices $B_i$, $i = 1, \dots, n$ (for a classical truss $k_i = 1$ and $B_i$ is the direction vector of bar $i$). A truss is a vector $t \in \mathbb R^n$ with $t \ge 0$ (the bar volumes) and a load is $f \in \mathbb R^m$. The bar-stiffness matrix is

$$A(t) = \sum_{i=1}^n t_i B_i B_i^T,$$

and the compliance is

$$\mathrm{Compl}_f(t) = \tfrac12 f^Tv \quad\text{where } A(t)v = f,$$

with $\mathrm{Compl}_f(t) = +\infty$ when the equilibrium equation $A(t)v = f$ has no solution; the value does not depend on which solution $v$ is used. For $t$ that are not nonnegative the compliance is extended by $+\infty$. The potential energy of the loaded truss is $\mathcal C_{t,f}(v) = \tfrac12 v^TA(t)v - f^Tv$.

The ice cream cone is $\mathbf L^k = \{x \in \mathbb R^k : x_k \ge \sqrt{x_1^2 + \dots + x_{k-1}^2}\}$. A set $X \subset \mathbb R^N$ is conic quadratic representable (CQr) if there are finitely many inequalities $A_j(x; u) - b_j \in \mathbf L^{m_j}$, affine in $x$ and in additional variables $u \in \mathbb R^l$, such that $x \in X$ exactly when some $u$ satisfies all of them; a function with values in $\mathbb R \cup \{+\infty\}$ is CQr when its epigraph is. A linear vector inequality $Ax - b \in \mathbf K$ is almost solvable if for every $\varepsilon > 0$ some $b'$ with $\|b' - b\|_2 < \varepsilon$ makes $Ax - b' \in \mathbf K$ solvable.

Formalization targets

Goal: Proposition 3.4.5 (p. 127)

For all $t \in \mathbb R^n$, $f \in \mathbb R^m$ and $\tau \in \mathbb R$, $\mathrm{Compl}_f(t) \le \tau$ (extended compliance) if and only if there are vectors $s_i \in \mathbb R^{k_i}$ with

$$\text{(a)}\ \sum_{i=1}^n B_is_i = f, \qquad \text{(b)}\ \sum_{i=1}^n \frac{s_i^Ts_i}{2t_i} \le \tau, \qquad \text{(c)}\ t \ge 0,$$

where $0/0 = 0$ and $a/0 = +\infty$ for $a > 0$. In particular, $(t, f) \mapsto \mathrm{Compl}_f(t)$ is CQr.

Milestones

• Lemma 3.4.1 (p. 122): for a symmetric positive semidefinite $A$, the form $\tfrac12 v^TAv - b^Tv$ is bounded below iff it attains its minimum iff $Av = b$ is solvable; the minimizers are the solutions, and the minimum is $-\tfrac12 b^Tv$.
• Proposition 3.4.4 (p. 122): for $t \ge 0$, $\mathrm{Compl}_f(t)$ is finite iff $\mathcal C_{t,f}$ is bounded below, and then $-\mathrm{Compl}_f(t) = \min_v \mathcal C_{t,f}(v)$.
• Statement (O) (p. 124): with $B(t) = \sqrt2\,[\sqrt{t_1}B_1^T; \dots; \sqrt{t_n}B_n^T]$, the inequality $\tfrac12 v^TA(t)v - f^Tv + \tau \le 0$ has no solution iff $\|(B(t)v;\ 1 - f^Tv + \tau)\|_2 \le 1 + f^Tv - \tau$ has none.
• Proposition 2.4.2 (pp. 61–62): for a pointed closed convex cone $\mathbf K$ with nonempty interior, $Ax - b \in \mathbf K$ is not almost solvable iff some $\lambda \in \mathbf K_*$ has $A^T\lambda = 0$ and $\lambda^Tb > 0$ (with parts (i) and (ii)).
• Statement (!!) (p. 125): for $t \ge 0$, $\mathrm{Compl}_f(t) < \tau$ iff the conic quadratic inequality above is not almost solvable.
• Lemma 3.4.2 (p. 126): for $t \ge 0$, $\mathrm{Compl}_f(t) < \tau$ iff some $\lambda \in \mathbf L^k$ has $A^T\lambda = 0$ and $b^T\lambda > 0$, for the explicit $A$, $b$ of (3.4.49).
• Lemma 3.4.3 (p. 127): for $t \ge 0$, $\mathrm{Compl}_f(t) < \tau$ iff some $s_i$ satisfy $\sum_i B_is_i = f$ and $\sum_i s_i^Ts_i/(2t_i) < \tau$.

Significance

The proposition gives an explicit second-order cone description of the epigraph of the compliance, jointly in the design $t$ and the load $f$. Consequences: single-load, multiload and volume-constrained truss design problems become conic quadratic programs solvable by interior-point methods; the compliance is a convex function of $(t, f)$; and the proposition contains a second variational principle (the reaction forces $s_i$ minimize the stored energy subject to equilibrium, p. 128). It also explains the linear-programming formulation of Lecture 1.

The results are classical and proved in the book; none of them is machine-checked. A formalization adds checked statements of the variational principle for positive semidefinite quadratic forms, the conic theorem of the alternative for almost solvability, and a first instance of conic quadratic representability on the platform, with the $0/0$ convention made explicit.

Difficulty

The compliance is defined through solvability of a singular linear system, so neither convexity nor any representation is visible from the definition. The equivalence in the goal must handle trusses with missing bars ($t_i = 0$), where $A(t)$ is singular and the convention $a/0 = +\infty$ matters, and loads outside the range of $A(t)$, where the compliance is infinite. The book's route goes through a conic theorem of the alternative, which in the conic case characterizes only almost solvability, not solvability; passing from the strict epigraph to the non-strict one in the goal requires a separate attainment argument. A step-by-step translation must keep track of the perturbations of the right-hand side.

Formalization scope

Vectors are functions on finite index types (Fin m → ℝ, Fin n → ℝ, Fin (k i) → ℝ); the stacked inequality of (3.4.49) is indexed by the pairs $(i, j)$, $j < k_i$, followed by two extra coordinates, the last of which is the distinguished coordinate of $\mathbf L^k$. The compliance takes values in EReal: ⊤ exactly when $A(t)v = f$ is unsolvable, and otherwise the real number $\tfrac12 f^Tv$; it only ever appears in comparisons with a real $\tau$. The convention $0/0 = 0$, $a/0 = +\infty$ is encoded by requiring $s_i = 0$ whenever $t_i = 0$ together with Lean's real division; Lean's $x/0 = 0$ alone would let a missing bar carry any force, and this trivializing reading is ruled out. The CQr conclusion is not "some representation exists" in an unconstrained sense: it is a finite system of Lorentz-cone constraints $A_j(x; u) - b_j \in \mathbf L^{m_j}$, $m_j \ge 2$, affine in the variables, exactly as on p. 86. Proposition 2.4.2 carries the book's standing assumptions: a pointed closed convex cone with nonempty interior, and Assumption A (full column rank of $A$, p. 53, in force by Remark 2.4.1).

Beyond the paper. One variant is posed: a strengthened Proposition 2.4.2 without Assumption A and on arbitrary finite index sets. Evidence: the systems involved depend on $A$ only through its column space, so a basis of that space reduces the general case to the stated one. This is the form actually used on p. 126, where the matrix of (3.4.49) can fail Assumption A (for example $t = 0$, $f = 0$), a gap in the printed argument recorded as a finding.

Needed infrastructure: positive semidefinite quadratic forms and their minimization (Mathlib's Matrix.PosSemidef), dual cones and separation in finite dimension, the ice cream cone and its self-duality, and continuity of minimum values of quadratic forms under perturbation. The definitions of the Lorentz cone, CQr sets and functions, and almost solvability are reusable across the series. Proofs of individual milestones are welcome independently; Lemma 3.4.1 and statement (O) are self-contained.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, MPS/SIAM Series on Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829
• M. P. Bendsøe, O. Sigmund, Topology Optimization: Theory, Methods, and Applications, Springer, 2003. https://doi.org/10.1007/978-3-662-05086-6