Theorem 4.2 — Under H1–H3 the SDP (15) has quadratic growth at every optimum and a unique solution

Proved

RobustSDP.Uniqueness.theorem_4_2

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1quadratic-growthrobust-optimizationsemidefinite-programminguniqueness

Consider the semidefinite program in the variables $(x,\tau) \in \mathbb{R}^m \times \mathbb{R}$ ,

\text{minimize } c^T x \quad\text{subject to}\quad \begin{bmatrix} F(x) - \tau L L^T & R(x)^T \\ R(x) & \tau I \end{bmatrix} \succeq 0, \tag{15}

where $F(x) = F_0 + \sum_i x_i F_i$ with symmetric $F_i \in \mathbb{R}^{n\times n}$ , $R(x) = R_0 + \sum_i x_i R_i$ with $R_i \in \mathbb{R}^{q\times n}$ , $L \in \mathbb{R}^{n\times p}$ , and $c \in \mathbb{R}^m \setminus \{0\}$ . This is the robust counterpart of an uncertain SDP under full norm-bounded perturbations with $D = 0$ and $\rho = 1$ .

Assume

H1: (15) is strictly feasible;
H2: (15) is inf-compact: every sublevel set $\{(x,\tau) \text{ feasible} : c^Tx \le M\}$ is bounded;
H3(a): the nullspace of $\lambda R_0 + \sum_i x_i R_i$ is the same proper subspace of $\mathbb{R}^n$ for all $(\lambda, x) \ne (0,0)$ ;
H3(b): $\begin{bmatrix} L^T \\ R(x)\end{bmatrix}$ has full column rank for every $x$ .

Then (15) satisfies the quadratic growth condition at every optimal point $y_{\mathrm{opt}} = (x_{\mathrm{opt}}, \tau_{\mathrm{opt}})$ : there are $\alpha, \varepsilon > 0$ such that every feasible $y = (x, \tau)$ with $\|y - y_{\mathrm{opt}}\| < \varepsilon$ satisfies

c^T x \ \ge\ c^T x_{\mathrm{opt}} + \alpha \|y - y_{\mathrm{opt}}\|^2 .

Consequently (15) has exactly one optimal point $(x, \tau)$ .

Uniqueness of the robust solution is what makes robustification a regularization of ill-posed SDPs, and quadratic growth is the property from which the paper's Hölder-stability results follow.

Formalization Note The conclusion has both parts of the theorem: quadratic growth at every optimal point, and existence and uniqueness of the optimal pair $(x,\tau)$ (existence is part of the paper's claim, via H1 and H2). $\|\cdot\|$ is the Euclidean norm on $\mathbb{R}^{m+1}$ ; the paper's $o(\|y - y_{\mathrm{opt}}\|^2)$ form of the QGC is equivalent to this local form. The QGC is stated for (15) rather than for the paper's reformulation (16), with which it agrees near $y_{\mathrm{opt}}$ because $\tau_{\mathrm{opt}} > 0$ . The standing assumptions $c \neq 0$ (p. 33) and symmetry of $F_0, \dots, F_m$ (p. 33) are explicit hypotheses.

Preamble

import Mathlib
import Definitions.Def_RobustSDP_Uniqueness_Model
import Definitions.Def_RobustSDP_Uniqueness_Hypotheses

open Matrix

Formal statement

namespace RobustSDP.Uniqueness

/-- **Theorem 4.2** (El Ghaoui–Oustry–Lebret 1998, p. 39). If H1–H3 hold, the SDP (15) satisfies the
quadratic growth condition at every optimal point `y_opt = (x_opt, τ_opt)`; consequently (15) has
a unique solution `(x, τ)`. Standing assumptions: `c ≠ 0` and `F₀, …, F_m` symmetric (p. 33). -/
theorem theorem_4_2 {m n p q : ℕ} (D : SDPData m n p q) (c : Fin m → ℝ) (hc : c ≠ 0)
    (hsym : D.Symmetric) (h1 : D.Slater) (h2 : D.InfCompact c) (h3a : D.H3a) (h3b : D.H3b) :
    (∀ y : (Fin m → ℝ) × ℝ, D.IsOptimal c y → D.QGC c y) ∧
      ∃! y : (Fin m → ℝ) × ℝ, D.IsOptimal c y := by sorry

end RobustSDP.Uniqueness

Source

El Ghaoui, Oustry and Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1) (1998), p. 39, Theorem 4.2 (with Eq. (15) and Hypotheses H1–H3, p. 38; proof in Appendix A, pp. 48–50)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $m, n, p, q$ be arbitrary natural numbers. The statement then takes three inputs:

Data $D$ . $D$ is an object of type SDPData m n p q, which is defined in the imported module Definitions.Def_RobustSDP_Uniqueness_Model. That definition is not part of the code given to this audit. Its fields, and how $m, n, p, q$ enter it (for example as matrix dimensions or numbers of blocks), cannot be read from the statement.
Vector $c$ . $c \in \mathbb{R}^m$ is a real vector indexed by $\{0, \dots, m-1\}$ .
Candidate points $y$ . These are pairs $y = (x, \tau)$ with $x \in \mathbb{R}^m$ and $\tau \in \mathbb{R}$ , so they live in $\mathbb{R}^m \times \mathbb{R}$ .

The theorem assumes all six of the following hypotheses:

$c \neq 0$ , meaning $c$ is not the zero vector of $\mathbb{R}^m$ .
$D$ satisfies the predicate Symmetric.
$D$ satisfies the predicate Slater.
$D$ satisfies the predicate InfCompact relative to $c$ .
$D$ satisfies the predicate H3a.
$D$ satisfies the predicate H3b.

The last five predicates come from the imported modules Definitions.Def_RobustSDP_Uniqueness_Model and Definitions.Def_RobustSDP_Uniqueness_Hypotheses. Their definitions are not included in the audited code. This read-back therefore cannot say which conditions on $D$ and $c$ they impose. In particular, it cannot say whether they can all hold at once, or how they depend on $n, p, q$ . The only thing visible is that InfCompact depends on $c$ and the other four do not. The docstring gives the statement a paper-theorem label and an informal gloss. That text is a comment, not part of the formal assertion, and nothing here is based on it.

The conclusion is the conjunction of two claims. Both use IsOptimal and QGC, which are also defined in the imported modules and not shown here. Write $\mathrm{Opt}_{D,c}(y)$ for " $y$ satisfies IsOptimal for $D$ and $c$ ", and $\mathrm{QGC}_{D,c}(y)$ for " $y$ satisfies QGC for $D$ and $c$ ".

(a) Every pair that satisfies IsOptimal also satisfies QGC:

\forall\, y \in \mathbb{R}^m \times \mathbb{R}:\quad \mathrm{Opt}_{D,c}(y) \;\Longrightarrow\; \mathrm{QGC}_{D,c}(y).

(b) There is exactly one pair $y = (x, \tau) \in \mathbb{R}^m \times \mathbb{R}$ with $\mathrm{Opt}_{D,c}(y)$ :

\exists!\, y \in \mathbb{R}^m \times \mathbb{R}:\quad \mathrm{Opt}_{D,c}(y).

This asserts both that such a pair exists and that it is unique. Uniqueness is of the whole pair, so both the $x$ -part and the $\tau$ -part are unique.

Degenerate cases:

$m = 0$ . Then $\mathbb{R}^0$ has exactly one element, the empty vector, and that element is the zero vector. So the hypothesis $c \neq 0$ cannot be satisfied, and the theorem says nothing (it is vacuously true) when $m = 0$ .
$m \geq 1$ . The hypothesis $c \neq 0$ can be satisfied.
$n$ , $p$ or $q$ equal to zero, and junk values. What happens here depends entirely on the imported definitions of SDPData, Symmetric, Slater, InfCompact, H3a, H3b, IsOptimal and QGC. None of them is visible. So this read-back cannot say:
- whether any of the six hypotheses fails, or holds trivially, when those dimensions are zero;
- whether those definitions involve total-function default values, such as division by zero, subtraction in $\mathbb{N}$ , or infima or suprema of empty or unbounded sets, that could make the hypotheses or conclusions vacuous.
The six hypotheses together. If they can never all hold at once for some choice of $m, n, p, q$ , the theorem is vacuous for that choice. The code shown does not settle whether this happens.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph