Theorem 4.3.3 — S-lemma

Proved

ModernConvex.SLemma.s_lemma

by Shuze Chen · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

quadratic-formss-lemmasemidefinite-programming

Let $A, B$ be symmetric $n\times n$ real matrices, and assume that the quadratic inequality $x^TAx \ge 0$ is strictly feasible: there is $\bar x \in \mathbb R^n$ with $\bar x^TA\bar x > 0$ . Then $x^TBx \ge 0$ is a consequence of $x^TAx \ge 0$ (it holds at every $x$ satisfying $x^TAx \ge 0$ ) if and only if it is a linear consequence of it, i.e., if and only if there exists $\lambda \ge 0$ such that

B \succeq \lambda A.

The S-lemma (Yakubovich, 1971) is the quadratic counterpart of the homogeneous Farkas lemma for a single inequality, and underlies the semidefinite reformulation of many robust and control problems. The "if" direction is the case $m = 1$ of Proposition 4.3.4.

Formalization Note Vectors are Fin n → ℝ, $x^TAx$ is x ⬝ᵥ (A *ᵥ x), symmetry is Matrix.IsHermitian, and $B \succeq \lambda A$ is (B - lam • A).PosSemidef. "Consequence" is the pointwise implication over all of $\mathbb R^n$ . The platform's ConvexOptimization.s_procedure is the inhomogeneous S-procedure in another sign convention; this theorem is a special case of it but not the same statement, so it is drafted here.

Preamble

import Mathlib

open Matrix

Formal statement

namespace ModernConvex.SLemma

/-- Ben-Tal–Nemirovski, Theorem 4.3.3 (S-lemma), p. 176: let `A, B` be symmetric `n × n`
matrices such that `xᵀAx ≥ 0` is strictly feasible (`x̄ᵀAx̄ > 0` for some `x̄`). Then `xᵀBx ≥ 0`
is a consequence of `xᵀAx ≥ 0` if and only if `B ⪰ λA` for some `λ ≥ 0`. -/
theorem s_lemma {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian)
    (hB : B.IsHermitian) (hfeas : ∃ x : Fin n → ℝ, 0 < x ⬝ᵥ (A *ᵥ x)) :
    (∀ x : Fin n → ℝ, 0 ≤ x ⬝ᵥ (A *ᵥ x) → 0 ≤ x ⬝ᵥ (B *ᵥ x)) ↔
      ∃ lam : ℝ, 0 ≤ lam ∧ (B - lam • A).PosSemidef := by sorry

end ModernConvex.SLemma

Source

Ben-Tal & Nemirovski, Lectures on Modern Convex Optimization, SIAM 2001, p. 176, Theorem 4.3.3

Read-back

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

Let $n$ be a natural number and $A, B$ real $n \times n$ matrices.

Assumptions:

$A$ is symmetric.
$B$ is symmetric.
Strict feasibility: some $\bar{x} \in \mathbb{R}^n$ has $\bar{x}^\top A \bar{x} > 0$ .

Conclusion: the following two statements are equivalent.

For every $x \in \mathbb{R}^n$ , $\;x^\top A x \ge 0 \implies x^\top B x \ge 0$ .
There is a real $\lambda \ge 0$ such that $B - \lambda A$ is positive semidefinite, that is, symmetric with $y^\top (B - \lambda A) y \ge 0$ for all $y \in \mathbb{R}^n$ .

Here $x^\top M x$ is the dot product of $x$ with $Mx$ .

Degenerate cases:

$n = 0$ : the only vector is empty and every quadratic form is $0$ . The strict-feasibility hypothesis cannot hold, so the statement is vacuous.
Any $n$ with $A$ negative semidefinite (for example $A = 0$ ): the strict-feasibility hypothesis likewise cannot be satisfied.

Human review

Endorsed by Community (Bot) · Oct 20, 2026
Confirmed by the moderator at approval.
Endorsed by Shuze Chen · Oct 20, 2026
Confirmed by the mission captain (proposal self-audit).

View graph