Complementary slackness

Proved

ConvexOptimization.complementary_slackness

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

convexoptimizationdualitykkt

Complementary slackness — condition (5.48) of Boyd & Vandenberghe.

For the standard problem, let $x^{\star}$ be feasible, let $\lambda \in \mathbb{R}^m$ with $\lambda \succeq 0$ and $\nu \in \mathbb{R}^p$ , and suppose the duality gap vanishes, $g(\lambda,\nu) = f_0(x^{\star})$ , where $g$ is the Lagrange dual function. Then

\lambda_i\, f_i(x^{\star}) \;=\; 0 \qquad (i = 1,\dots,m).

Equivalently: $\lambda_i > 0 \Rightarrow f_i(x^{\star}) = 0$ and $f_i(x^{\star}) < 0 \Rightarrow \lambda_i = 0$ . A constraint that is slack at the optimum carries no price, and a constraint with a positive price is active.

Beyond being one of the four KKT conditions, this is the result that gives dual variables their economic reading as shadow prices, and in practice it is what lets an algorithm identify the active set from a dual solution. No convexity is required: the hypothesis is a zero gap, however obtained.

Formalization Note The zero-gap hypothesis equates the EReal-valued dual function with the coercion of the real number $f_0(x^{\star})$ , which also encodes finiteness of $g(\lambda,\nu)$ ; feasibility of $x^{\star}$ is membership in the mission's feasible-set definition. Source: B&V §5.5.2, p. 242, eq. (5.48).

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.complementary_slackness {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)) (hxs : xs ∈ feasibleSet fc a b)
    (lam : Fin mm → ℝ) (hlam : ∀ i, 0 ≤ lam i) (nu : Fin p → ℝ)
    (hzero : dualFunction f₀ fc a b lam nu = (f₀ xs : EReal)) :
    ∀ i, lam i * fc i xs = 0 := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 242, §5.5.2 eq. (5.48) (complementary slackness)

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 regularity assumptions), a point $x_s$ that is feasible ( $f_i(x_s) \le 0$ for every $i$ and $\langle a_j, x_s\rangle = b_j$ for every $j$ ), multipliers $\lambda$ with $\lambda_i \ge 0$ for every $i$ , $\nu$ unrestricted, and assume the exact extended-real equality

g(\lambda, \nu) \;=\; f_0(x_s),

i.e. the unconstrained infimum over $x \in \mathbb{R}^n$ of the Lagrangian $f_0(x) + \sum_i \lambda_i f_i(x) + \sum_j \nu_j(\langle a_j,x\rangle - b_j)$ , computed in $[-\infty,+\infty]$ , equals the (finite) value $f_0(x_s)$ — in particular the hypothesis rules out $g(\lambda,\nu) = -\infty$ . The conclusion is: for every $i \in \{0,\dots,mm-1\}$ , the exact real equality $\lambda_i \cdot f_i(x_s) = 0$ holds (so for each $i$ , either $\lambda_i = 0$ or $f_i(x_s) = 0$ ). When $mm = 0$ the conclusion is vacuous.

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