Strict LMI theorem of alternatives

Proved

ConvexOptimization.lmi_strict_alternative

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

convex-optimizations-proceduresemidefinite-programming

Theorem of alternatives for a strict linear matrix inequality — example 5.14 of Boyd & Vandenberghe.

Let $F_1,\dots,F_n, G$ be symmetric $k \times k$ real matrices and write $F(x) = G + \sum_{i=1}^{n} x_i F_i$ . Then exactly one of the following two systems is feasible:

\exists x \in \mathbb{R}^n:\ F(x) \prec 0 \qquad\text{versus}\qquad \exists Z \in \mathbb{S}^{k}:\ Z \succeq 0,\ Z \ne 0,\ \operatorname{tr}(F_i Z) = 0 \ (i = 1,\dots,n),\ \operatorname{tr}(GZ) \ge 0 .

They are strong alternatives — never both feasible, never both infeasible.

The second system is a certificate that no $x$ makes $F(x)$ negative definite: a nonzero positive semidefinite $Z$ orthogonal to every $F_i$ and non-negatively paired with $G$ . This is the semidefinite instance of the conic theorem of alternatives, obtained by taking $K$ to be the positive semidefinite cone, and it is the tool that reduces feasibility questions about LMIs — ubiquitous in control theory — to a search for such a $Z$ .

Formalization Note $F(x) \prec 0$ is written (-(G + ∑ i, x i • F i)).PosDef and $Z \succeq 0$ as Z.PosSemidef; the trace pairings use (F i * Z).trace. The statement is an iff between the first system and the negation of the second. Source: B&V §5.9.4, example 5.14, pp. 270–271.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.lmi_strict_alternative {n nn : ℕ}
    (F : Fin n → Matrix (Fin nn) (Fin nn) ℝ) (hF : ∀ i, (F i).IsSymm)
    (G : Matrix (Fin nn) (Fin nn) ℝ) (hG : G.IsSymm) :
    (∃ x : Fin n → ℝ, (-(G + ∑ i, x i • F i)).PosDef) ↔
      ¬∃ Z : Matrix (Fin nn) (Fin nn) ℝ, Z.PosSemidef ∧ Z ≠ 0 ∧
        (∀ i, ((F i) * Z).trace = 0) ∧ 0 ≤ (G * Z).trace := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 270, §5.9.4 example 5.14 (feasibility of a strict linear matrix inequality: strong alternatives)

Read-back

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

Theorem. Fix natural numbers $n$ , $nn$ ; matrices $F_1,\dots,F_n$ and $G$ , all real $nn\times nn$ and each assumed symmetric. With no further hypotheses (no boundedness, no constraint qualification), the theorem asserts the equivalence:

\Big(\exists\, x \in \mathbb{R}^n:\ -\big(G + \textstyle\sum_i x_i F_i\big) \text{ is positive definite}\Big) \iff \neg\Big(\exists\, Z \in \mathbb{R}^{nn\times nn}:\ Z \text{ positive semidefinite},\ Z \ne 0,\ \operatorname{tr}(F_i Z) = 0 \ \forall i,\ \text{and}\ 0 \le \operatorname{tr}(G Z)\Big).

Mathlib's positive (semi)definiteness includes the symmetry requirement; $\operatorname{tr}(MZ) = \sum_{k,\ell} M_{k\ell} Z_{\ell k}$ . Note the trace inequality on the alternative side is nonstrict ( $0 \le \operatorname{tr}(GZ)$ ) and the alternative explicitly requires $Z \ne 0$ . Edge cases: for $nn = 0$ , positive definiteness is vacuously true (any $x$ works, e.g. the left side holds), and the only $0\times 0$ matrix is $Z = 0$ , so $Z \ne 0$ is unsatisfiable and the right side is also vacuously true — the biconditional holds degenerately. For $n = 0$ the sum is empty, the left side reads " $-G$ is positive definite", and the trace conditions $\operatorname{tr}(F_i Z)=0$ are vacuous.

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