Saddle-point characterization of strong duality

Proved

ConvexOptimization.lagrangian_saddle_iff_strong_duality

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

convexoptimizationdualitykkt

The saddle-point characterization of strong duality.

For the standard problem, write $L(x,\lambda,\nu) = f_0(x) + \sum_i \lambda_i f_i(x) + \sum_j \nu_j(\langle a_j,x\rangle - b_j)$ and $g(\lambda,\nu) = \inf_x L(x,\lambda,\nu)$ . Fix $x^{\star} \in \mathbb{R}^n$ , $\lambda \in \mathbb{R}^m$ with $\lambda \succeq 0$ , and $\nu \in \mathbb{R}^p$ . Then $(x^{\star},(\lambda,\nu))$ is a saddle point of $L$ — i.e.

L(x^{\star},\lambda',\nu') \;\le\; L(x^{\star},\lambda,\nu) \;\le\; L(x,\lambda,\nu) \qquad \text{for all } \lambda' \succeq 0,\ \nu' \in \mathbb{R}^p,\ x \in \mathbb{R}^n

— if and only if $x^{\star}$ is feasible, $x^{\star}$ minimizes $f_0$ over the feasible set, and $g(\lambda,\nu) = f_0(x^{\star})$ , i.e. the duality gap is zero.

The equivalence identifies "zero gap with attained optima" with a purely pointwise property of a single function, and it is the step that yields stationarity: at a zero-gap pair, $x^{\star}$ minimizes $L(\cdot,\lambda,\nu)$ over the whole space, so for differentiable data its gradient there vanishes — which is precisely the last KKT condition. It also connects this theory to minimax duality, since a saddle point is exactly a point where $\inf\sup$ and $\sup\inf$ agree.

Formalization Note The supremum side of the saddle condition is written as a universally quantified inequality over dual-feasible $(\lambda',\nu')$ rather than as a supremum, avoiding extended-real arithmetic on that side; the zero-gap condition compares the EReal-valued dual function with the coercion of $f_0(x^{\star})$ . Source: B&V §5.4.2, pp. 239–240.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.lagrangian_saddle_iff_strong_duality {n mm p : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ)
    (fc : Fin mm → EuclideanSpace ℝ (Fin n) → ℝ)
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (b : Fin p → ℝ)
    (xs : EuclideanSpace ℝ (Fin n)) (lam : Fin mm → ℝ) (hlam : ∀ i, 0 ≤ lam i)
    (nu : Fin p → ℝ) :
    ((∀ (lam' : Fin mm → ℝ), (∀ i, 0 ≤ lam' i) → ∀ nu' : Fin p → ℝ,
        lagrangian f₀ fc a b xs lam' nu' ≤ lagrangian f₀ fc a b xs lam nu) ∧
     (∀ x, lagrangian f₀ fc a b xs lam nu ≤ lagrangian f₀ fc a b x lam nu)) ↔
    (xs ∈ feasibleSet fc a b ∧ IsMinOn f₀ (feasibleSet fc a b) xs ∧
     dualFunction f₀ fc a b lam nu = (f₀ xs : EReal)) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 239-240, §5.4.2 (saddle-point interpretation; the max-min characterization of strong duality)

Read-back

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

Theorem. Fix data $f_0, f, a, b$ (implicit $n, mm, p$ ; no convexity, continuity, or differentiability assumed), a point $x_s \in \mathbb{R}^n$ , multipliers $\lambda \in \mathbb{R}^{mm}$ with the standing hypothesis $\lambda_i \ge 0$ for every $i$ (this is assumed outside the equivalence, so it is available in both directions), and $\nu \in \mathbb{R}^p$ unrestricted. Writing $L(x,\lambda,\nu) = f_0(x) + \sum_i \lambda_i f_i(x) + \sum_j \nu_j(\langle a_j,x\rangle - b_j)$ for the (real-valued) Lagrangian and $g(\lambda,\nu) = \inf_{x\in\mathbb{R}^n} L(x,\lambda,\nu)$ (in the extended reals) for the dual function, the theorem is the equivalence of:

Left side (saddle point): both (i) for every $\lambda' \in \mathbb{R}^{mm}$ with $\lambda'_i \ge 0$ for all $i$ and every $\nu' \in \mathbb{R}^p$ , $L(x_s, \lambda', \nu') \le L(x_s, \lambda, \nu)$ ; and (ii) for every $x \in \mathbb{R}^n$ (unconstrained, the whole space), $L(x_s, \lambda, \nu) \le L(x, \lambda, \nu)$ .
Right side: the conjunction of (i) $x_s$ is feasible, i.e. $f_i(x_s) \le 0$ for all $i$ and $\langle a_j, x_s\rangle = b_j$ for all $j$ ; (ii) $f_0(x_s) \le f_0(x)$ for every feasible $x$ ; and (iii) the exact extended-real equality $g(\lambda, \nu) = f_0(x_s)$ . All inequalities are non-strict. Edge cases: when $mm = p = 0$ the saddle condition (i) on the left is trivially an equality, feasibility is vacuous, and the content reduces to $x_s$ being an unconstrained global minimizer of $f_0$ with $\inf f_0$ attained at $x_s$ .

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