Trust-region strong duality (level-set form)

Proved

ConvexOptimization.single_constraint_quadratic_strong_duality

by Shuze Chen · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-optimizations-proceduresemidefinite-programming

Zero duality gap for minimizing one quadratic function subject to another — the strong-duality result of B&V §B.1.

Let $q_k(x) = x^{T}A_k x + 2b_k^{T}x + c_k$ for $k = 0, 1$ with $A_0, A_1$ symmetric, and assume strict feasibility: some $\hat{x}$ has $q_1(\hat{x}) < 0$ . Then for every $\gamma \in \mathbb{R}$ ,

\bigl(q_1(x) \le 0 \Rightarrow q_0(x) \ge \gamma \ \text{ for all } x\bigr) \qquad\Longleftrightarrow\qquad \exists\,\lambda \ge 0:\ \begin{bmatrix} A_0 & b_0 \\ b_0^{T} & c_0 - \gamma\end{bmatrix} + \lambda \begin{bmatrix} A_1 & b_1 \\ b_1^{T} & c_1 \end{bmatrix} \;\succeq\; 0 .

Read as an optimization statement: $\gamma$ is a lower bound for the (generally nonconvex) problem of minimizing $q_0$ subject to $q_1 \le 0$ exactly when it is achievable by the semidefinite relaxation, so the two optimal values coincide and the Lagrangian relaxation is tight. This is remarkable — the primal problem need not be convex, $A_0$ and $A_1$ may be indefinite — and it is the theoretical basis of trust-region methods, where a quadratic model is minimized over a ball.

Formalization Note The quadratics and their block matrices are the mission's quadForm and symQuadBlock; the matrix inequality is PosSemidef of the sum. The statement is corrected for the factor-of-two slips in the printed eq. (B.5). In the book this result is derived from the S-procedure (§B.4), so it is a consequence of the mission's goal rather than a step toward it. Source: B&V §B.1, p. 654, proof in §B.4, p. 658.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_quadraticForms

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.single_constraint_quadratic_strong_duality {nn : ℕ}
    (A₀ A₁ : Matrix (Fin nn) (Fin nn) ℝ) (hA₀ : A₀.IsSymm) (hA₁ : A₁.IsSymm)
    (b₀ b₁ : Fin nn → ℝ) (c₀ c₁ : ℝ)
    (xh : Fin nn → ℝ) (hxh : quadForm A₁ b₁ c₁ xh < 0) (γ : ℝ) :
    (∀ x, quadForm A₁ b₁ c₁ x ≤ 0 → γ ≤ quadForm A₀ b₀ c₀ x) ↔
      ∃ lam : ℝ, 0 ≤ lam ∧
        (symQuadBlock A₀ b₀ (c₀ - γ) + lam • symQuadBlock A₁ b₁ c₁).PosSemidef := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 653-654, 658, §B.1 eq. (B.1)-(B.2) (strong duality for one quadratic function constrained by another), proof in §B.4. Formalized with the printed factor-of-2 slips in eq. (B.5) corrected. Note the book derives this result FROM the S-procedure, so it is a corollary of this mission's goal

Read-back

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

Theorem. Fix a natural number $nn$ ; real $nn\times nn$ matrices $A_0$ , $A_1$ , each assumed symmetric; vectors $b_0, b_1 \in \mathbb{R}^{nn}$ ; scalars $c_0, c_1 \in \mathbb{R}$ ; a point $x_h \in \mathbb{R}^{nn}$ with $q_1(x_h) < 0$ (strict), where the file's ConvexOptimization_quadForm unfolds as $q_k(x) := x^\top A_k x + 2\,(b_k \cdot x) + c_k$ (note the factor $2$ on the linear term); and an arbitrary scalar $\gamma \in \mathbb{R}$ (a free parameter, with no hypothesis on it). No convexity or definiteness is assumed of $A_0$ or $A_1$ — the quadratics may be indefinite. The theorem asserts the equivalence:

\Big(\forall x \in \mathbb{R}^{nn}:\ q_1(x) \le 0 \implies \gamma \le q_0(x)\Big) \iff \Big(\exists\, \lambda \in \mathbb{R}:\ 0 \le \lambda \ \wedge\ M_0 + \lambda M_1 \text{ is positive semidefinite}\Big),

where, unfolding the file's ConvexOptimization_symQuadBlock, $M_0$ and $M_1$ are the $(nn+1)\times(nn+1)$ block matrices over the index type $\mathrm{Fin}\,nn \oplus \mathrm{Unit}$ ( $nn$ coordinates plus one extra index)

M_0 = \begin{pmatrix} A_0 & b_0 \\ b_0^\top & c_0 - \gamma \end{pmatrix}, \qquad M_1 = \begin{pmatrix} A_1 & b_1 \\ b_1^\top & c_1 \end{pmatrix};

the shift by $\gamma$ appears only in the bottom-right scalar entry of $M_0$ . Positive semidefiniteness in Mathlib includes the symmetry requirement (satisfied here since $A_0, A_1$ are symmetric). Both inequalities on the left are as written: nonstrict constraint $q_1(x) \le 0$ , nonstrict bound $\gamma \le q_0(x)$ ; on the right $\lambda \ge 0$ is nonstrict. Edge case: for $nn = 0$ the quadratics are the constants $c_k$ , the strict-feasibility hypothesis forces $c_1 < 0$ , the left side reads $(c_1 \le 0 \implies \gamma \le c_0)$ , and $M_0 + \lambda M_1$ is the $1\times 1$ matrix $\big(c_0 - \gamma + \lambda c_1\big)$ .

Human review

Endorsed by Community (Bot) · Aug 13, 2026
Endorsed by Shuze Chen · Aug 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph