Conic strong duality under generalized Slater

Proved

ConvexOptimization.conic_slater_strong_duality

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

convex-optimizations-proceduresemidefinite-programming

Strong duality for cone programs under a generalized Slater condition.

Let $K \subseteq \mathbb{R}^d$ be a closed convex cone with dual cone $K^{*}$ , and consider

\text{minimize } f_0(x) \quad\text{subject to}\quad f(x) \preceq_K 0, \quad \langle a_j, x\rangle = b_j \ (j = 1,\dots,p),

where $f_0 : \mathbb{R}^n \to \mathbb{R}$ is convex, $f : \mathbb{R}^n \to \mathbb{R}^d$ is $K$ -convex — meaning $\theta f(x) + (1-\theta)f(y) - f(\theta x + (1-\theta)y) \in K$ for $\theta \in [0,1]$ — and $a_1,\dots,a_p$ are linearly independent. Assume the generalized Slater condition: some $\tilde{x}$ satisfies the equality constraints and has $-f(\tilde{x})$ in the interior of $K$ . If the optimal value $p^{\star}$ is finite, then the dual optimum is attained: there exist $z \in K^{*}$ and $\nu \in \mathbb{R}^p$ with

\inf_{x \in \mathbb{R}^n}\Bigl[f_0(x) + \langle z, f(x)\rangle + \sum_{j=1}^{p}\nu_j\bigl(\langle a_j,x\rangle - b_j\bigr)\Bigr] \;=\; p^{\star} .

This is Slater's theorem with the componentwise inequality $f_i(x) \le 0$ replaced by a generalized inequality with respect to $K$ , and the multiplier vector $\lambda \succeq 0$ replaced by a dual-cone vector $z \in K^{*}$ . Specializing $K$ to the positive semidefinite cone gives semidefinite programming duality and the LMI theorems of alternatives; specializing to the nonnegative orthant recovers the ordinary case.

Formalization Note The cone is given by explicit convexity, closedness and positive-scaling hypotheses rather than by a bundled structure, and $K$ -convexity of $f$ is stated as the displayed membership; $p^{\star}$ appears as an sInf over the image of the feasible set with an accompanying BddBelow hypothesis. Source: B&V §5.9.1–5.9.2, pp. 264–266.

Preamble

import Mathlib
import Definitions.Def_dualCone

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.conic_slater_strong_duality {n d p : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ) (hf₀ : ConvexOn ℝ Set.univ f₀)
    (K : Set (EuclideanSpace ℝ (Fin d))) (hKconv : Convex ℝ K)
    (hKclosed : IsClosed K) (hKcone : ∀ t : ℝ, 0 < t → ∀ y ∈ K, t • y ∈ K)
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin d))
    (hf : ∀ x y : EuclideanSpace ℝ (Fin n), ∀ θ : ℝ, 0 ≤ θ → θ ≤ 1 →
      θ • f x + (1 - θ) • f y - f (θ • x + (1 - θ) • y) ∈ K)
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (ha : LinearIndependent ℝ a)
    (b : Fin p → ℝ)
    (xs : EuclideanSpace ℝ (Fin n)) (hxs_slater : -f xs ∈ interior K)
    (hxs_eq : ∀ j, ⟪a j, xs⟫ = b j)
    (hbdd : BddBelow (f₀ '' {x | -f x ∈ K ∧ ∀ j, ⟪a j, x⟫ = b j})) :
    ∃ (z : EuclideanSpace ℝ (Fin d)) (nu : Fin p → ℝ), z ∈ dualCone K ∧
      (⨅ x : EuclideanSpace ℝ (Fin n),
        ((f₀ x + ⟪z, f x⟫ + ∑ j, nu j * (⟪a j, x⟫ - b j) : ℝ) : EReal)) =
      ((sInf (f₀ '' {x | -f x ∈ K ∧ ∀ j, ⟪a j, x⟫ = b j}) : ℝ) : EReal) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 264-266, §5.9.1-§5.9.2 (Lagrange duality and strong duality for problems with generalized inequalities, under the generalized Slater condition)

Read-back

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

Theorem. Fix natural numbers $n$ , $d$ , $p$ . Assume: $f_0 : \mathbb{R}^n \to \mathbb{R}$ (total, real-valued) convex on all of $\mathbb{R}^n$ ; a set $K \subseteq \mathbb{R}^d$ that is convex, topologically closed, and closed under strictly positive scalings ( $t\,y \in K$ for all $t > 0$ , $y \in K$ — nothing is required at $t = 0$ , so $0 \in K$ is not directly assumed); a map $f : \mathbb{R}^n \to \mathbb{R}^d$ satisfying, for all $x, y \in \mathbb{R}^n$ and all $\theta \in [0,1]$ , the $K$ -convexity condition $\theta f(x) + (1-\theta) f(y) - f(\theta x + (1-\theta) y) \in K$ (note that taking $\theta = 0$ makes this expression the zero vector, so this hypothesis does force $0 \in K$ ); linearly independent vectors $a_1,\dots,a_p \in \mathbb{R}^n$ (so $p \le n$ ; vacuous for $p = 0$ ) and scalars $b_1,\dots,b_p$ ; a Slater point $x_s \in \mathbb{R}^n$ with $-f(x_s)$ in the topological interior of $K$ and $\langle a_j, x_s\rangle = b_j$ for every $j$ (since $\operatorname{int} K \subseteq K$ , the feasible set below contains $x_s$ and is nonempty); and the hypothesis that the value set $\{f_0(x) : -f(x) \in K \ \wedge\ \langle a_j,x\rangle = b_j\ \forall j\}$ is bounded below in $\mathbb{R}$ . Conclusion: there exist $z \in \mathbb{R}^d$ and $\nu \in \mathbb{R}^p$ such that (i) $z$ lies in the dual cone of $K$ , which unfolds to: $\langle x, z\rangle \ge 0$ for every $x \in K$ ; and (ii) the extended-real infimum over all $x \in \mathbb{R}^n$ (unconstrained)

\inf_{x \in \mathbb{R}^n}\Big(f_0(x) + \langle z, f(x)\rangle + \textstyle\sum_j \nu_j\,(\langle a_j,x\rangle - b_j)\Big)

equals, as an element of $\overline{\mathbb{R}} = [-\infty,+\infty]$ , the embedding of the real number $\inf\,\{f_0(x) : -f(x)\in K \wedge \langle a_j,x\rangle=b_j\ \forall j\}$ . The primal infimum is Lean's real-valued $\inf$ , which by convention returns the junk value $0$ on an empty or unbounded-below set — both excluded here by the Slater point and the boundedness hypothesis, so it is the genuine infimum. Because the right-hand side is a (finite) real number embedded into the extended reals, the equality forces the unconstrained dual infimum to be finite and exactly equal to the primal optimal value. No attainment of either infimum is asserted; $\nu$ is unrestricted in sign, and no condition beyond dual-cone membership is placed on $z$ . Edge cases: $d = 0$ collapses $\mathbb{R}^d$ to the one-point space, where $K$ is either $\varnothing$ or $\{0\}$ and the Slater condition requires $-f(x_s) \in \operatorname{int} K$ , i.e. $K$ must be the whole one-point space (whose interior is itself); $n = 0$ makes all infima run over the single point of $\mathbb{R}^0$ .

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