Theorem 5.3 — Complementary Slackness Theorem

Proved

VanderbeiLP.StrictComp.complementary_slackness

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

complementary-slacknessdualitylinear-programmingp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Consider the standard-form linear program "maximize $c^T x$ subject to $Ax \le b$ , $x \ge 0$ " with $A \in \mathbb{R}^{m \times n}$ , $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ , and its dual "minimize $b^T y$ subject to $A^T y \ge c$ , $y \ge 0$ ". Suppose $x = (x_1, \dots, x_n)$ is primal feasible and $y = (y_1, \dots, y_m)$ is dual feasible, and let

$w_i = b_i - \sum_j a_{ij} x_j$ ( $i = 1, \dots, m$ ) be the corresponding primal slack variables,
$z_j = \sum_i y_i a_{ij} - c_j$ ( $j = 1, \dots, n$ ) be the corresponding dual slack variables.

Then $x$ and $y$ are optimal for their respective problems if and only if

x_j z_j = 0 \ \ (j = 1, \dots, n), \qquad w_i y_i = 0 \ \ (i = 1, \dots, m). \qquad (5.7)

The theorem turns optimality into a finite system of equations, which is how an optimal dual solution is recovered from an optimal primal one.

Preamble

import Mathlib
import Definitions.Def_VanderbeiLP_StrictComp_PrimalDualPair

open Matrix

Formal statement

namespace VanderbeiLP.StrictComp

/-- **Vanderbei, Theorem 5.3 (p. 63).** Complementary slackness: for primal feasible `x` with
slack `w = b - Ax` and dual feasible `y` with slack `z = Aᵀy - c`, `x` and `y` are optimal
for their respective problems iff `xⱼzⱼ = 0` for all `j` and `wᵢyᵢ = 0` for all `i` (5.7). -/
theorem complementary_slackness {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ)
    (c : Fin n → ℝ) (x : Fin n → ℝ) (y : Fin m → ℝ)
    (hx : PrimalFeasible A b x) (hy : DualFeasible A c y) :
    (PrimalOptimal A b c x ∧ DualOptimal A b c y) ↔
      ((∀ j, x j * dualSlack A c y j = 0) ∧ ∀ i, primalSlack A b x i * y i = 0) := by sorry

end VanderbeiLP.StrictComp

Source

Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer 2014, p. 63, Theorem 5.3, Eq. (5.7) (PDF p. 79)

Human review

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

View graph