Prove2Me

Theorem 10.7 — Strict Complementary Slackness Theorem

Open
VanderbeiLP.StrictComp.strict_complementary_slackness

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

dualitylinear-programmingp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1strict-complementarity

Consider the linear program with explicit slacks

maximize cTx  subject to Ax+w=b, x,w≥0(10.9)\text{maximize } c^T x \ \text{ subject to } Ax + w = b,\ x, w \ge 0 \qquad (10.9)

and its dual

minimize bTy  subject to ATy−z=c, y,z≥0,(10.10)\text{minimize } b^T y \ \text{ subject to } A^T y - z = c,\ y, z \ge 0, \qquad (10.10)

with A∈Rm×nA \in \mathbb{R}^{m \times n}, b∈Rmb \in \mathbb{R}^m, c∈Rnc \in \mathbb{R}^n. If the primal problem has an optimal solution, then there are an optimal primal solution (x∗,w∗)(x^*, w^*) and an optimal dual solution (y∗,z∗)(y^*, z^*) such that

x∗+z∗>0andy∗+w∗>0,x^* + z^* > 0 \qquad \text{and} \qquad y^* + w^* > 0,

where ξ>0\xi > 0 means that every component of ξ\xi is strictly positive.

By complementary slackness (Theorem 5.3), for every optimal pair xj∗zj∗=0x^*_j z^*_j = 0 and yi∗wi∗=0y^*_i w^*_i = 0. The theorem says that the optimal pair can be chosen so that in each complementary pair exactly one member vanishes: the complementary slackness is strict. This is the Goldman–Tucker theorem (1956), written for Vanderbei's inequality-form pair.

Formalization Note "Optimal" means feasible and attaining the maximum (primal) or the minimum (dual) over the feasible set. The dual optimum is part of the conclusion: only a primal optimal solution is assumed. The slacks are w∗=b−Ax∗w^* = b - Ax^* and z∗=ATy∗−cz^* = A^T y^* - c. The book's remark after the theorem cites "the complementary slackness theorem (Theorem 5.1)"; the complementary slackness theorem is Theorem 5.3.

Preamble
import Mathlib
import Definitions.Def_VanderbeiLP_StrictComp_PrimalDualPair

open Matrix
Formal statement
namespace VanderbeiLP.StrictComp

/-- **Vanderbei, Theorem 10.7 (p. 149), Strict Complementary Slackness Theorem.** If the LP
(10.9) has an optimal solution, then there are a primal optimal `x*` (slack `w* = b - Ax*`) and
a dual optimal `y*` (slack `z* = Aᵀy* - c`) with `x* + z* > 0` and `y* + w* > 0`
componentwise. -/
theorem strict_complementary_slackness {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (c : Fin n → ℝ) (hopt : ∃ x : Fin n → ℝ, PrimalOptimal A b c x) :
    ∃ (xstar : Fin n → ℝ) (ystar : Fin m → ℝ),
      PrimalOptimal A b c xstar ∧ DualOptimal A b c ystar ∧
      (∀ j, 0 < xstar j + dualSlack A c ystar j) ∧
      (∀ i, 0 < ystar i + primalSlack A b xstar i) := by sorry

end VanderbeiLP.StrictComp
Source
Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer 2014, p. 149, Theorem 10.7 (PDF p. 162); Eqs. (10.9)–(10.10), p. 147; footnote 2, p. 148
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