Slater's theorem: strong duality with dual attainment

Proved

ConvexOptimization.slater_strong_duality

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

convexoptimizationdualitykkt

Slater's theorem: strong duality with dual attainment.

Consider the standard problem on $\mathbb{R}^n$ with objective $f_0$ , inequality constraints $f_i(x) \le 0$ $(i = 1,\dots,m)$ and equality constraints $\langle a_j, x\rangle = b_j$ $(j = 1,\dots,p)$ , and assume

$f_0$ and every $f_i$ are convex on $\mathbb{R}^n$ ;
the vectors $a_1,\dots,a_p$ are linearly independent (the full-rank condition on the equality constraints);
Slater's condition: there is a point $\tilde{x}$ with $f_i(\tilde{x}) < 0$ for every $i$ and $\langle a_j,\tilde{x}\rangle = b_j$ for every $j$ ;
the optimal value $p^{\star} = \inf\{f_0(x) : x \text{ feasible}\}$ is finite (the objective is bounded below on the feasible set).

Then the dual optimum is attained and the duality gap is zero: there exist $\lambda \in \mathbb{R}^m$ with $\lambda \succeq 0$ and $\nu \in \mathbb{R}^p$ such that

g(\lambda,\nu) \;=\; p^{\star} .

Strong duality is the deepest result of the chapter, and attainment is the part that matters here: the theorem does not merely close the gap in the limit, it produces an actual multiplier pair, and those multipliers are exactly the $\lambda^{\star},\nu^{\star}$ appearing in the KKT conditions. Slater's condition cannot simply be dropped — without an interior feasible point the gap can be strictly positive.

Formalization Note $p^{\star}$ appears as sInf (f₀ '' feasibleSet fc a b) and the boundedness hypothesis BddBelow is what makes that infimum meaningful rather than a junk value; the conclusion equates the EReal-valued dual function with the coercion of that real number, which also asserts finiteness of $g(\lambda,\nu)$ . Source: B&V §5.3.2, pp. 234–236, the book's separating-hyperplane proof.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.slater_strong_duality {n mm p : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ) (hf₀ : ConvexOn ℝ Set.univ f₀)
    (fc : Fin mm → EuclideanSpace ℝ (Fin n) → ℝ)
    (hfc : ∀ i, ConvexOn ℝ Set.univ (fc i))
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (ha : LinearIndependent ℝ a)
    (b : Fin p → ℝ)
    (xs : EuclideanSpace ℝ (Fin n)) (hxs_ineq : ∀ i, fc i xs < 0)
    (hxs_eq : ∀ j, ⟪a j, xs⟫ = b j)
    (hbdd : BddBelow (f₀ '' feasibleSet fc a b)) :
    ∃ (lam : Fin mm → ℝ) (nu : Fin p → ℝ), (∀ i, 0 ≤ lam i) ∧
      dualFunction f₀ fc a b lam nu =
        ((sInf (f₀ '' feasibleSet fc a b) : ℝ) : EReal) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 234-236, §5.3.2 (Slater's condition; proof of strong duality via a separating hyperplane). Formalized with the hypotheses the book's proof actually uses: convex data total on R^n, linearly independent equality rows, and a finite optimal value

Read-back

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

Theorem. Fix implicit $n, mm, p$ and assume: (a) $f_0 : \mathbb{R}^n \to \mathbb{R}$ is convex on the whole space $\mathbb{R}^n$ ; (b) each $f_i$ ( $i \in \{0,\dots,mm-1\}$ ) is convex on the whole space; (c) the family of vectors $(a_j)_{j < p}$ is linearly independent over $\mathbb{R}$ (vacuous when $p = 0$ ); (d) there exists a given "Slater point" $x_s \in \mathbb{R}^n$ with $f_i(x_s) < 0$ strictly for every $i$ (vacuous when $mm = 0$ ) and $\langle a_j, x_s\rangle = b_j$ exactly for every $j$ ; (e) the image set $\{f_0(x) : x \text{ feasible}\}$ is bounded below, where "feasible" means $f_i(x) \le 0$ for all $i$ and $\langle a_j, x\rangle = b_j$ for all $j$ . (Note $x_s$ itself is feasible, so this image is nonempty; together with (e), its real infimum $\inf\{f_0(x) : x \text{ feasible}\}$ is a genuine finite infimum rather than the junk value $0$ that the real-infimum operator returns on empty or unbounded sets.) The conclusion asserts the existence of multipliers $\lambda \in \mathbb{R}^{mm}$ and $\nu \in \mathbb{R}^p$ such that $\lambda_i \ge 0$ for every $i$ and, as an exact equality of extended reals,

g(\lambda, \nu) \;=\; \inf\{\, f_0(x) \mid x \text{ feasible} \,\},

where $g(\lambda,\nu) = \inf_{y \in \mathbb{R}^n}\bigl(f_0(y) + \sum_i \lambda_i f_i(y) + \sum_j \nu_j(\langle a_j,y\rangle - b_j)\bigr)$ in $[-\infty,+\infty]$ and the right-hand side is a real number coerced into the extended reals (so the equality in particular forces $g(\lambda,\nu)$ to be finite). This asserts both zero duality gap and attainment of the dual optimum at some $(\lambda,\nu)$ ; it does not assert attainment of the primal infimum, uniqueness of $(\lambda,\nu)$ , or anything about $\nu$ 's sign. No differentiability is assumed.

Human review

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

View graph