Theorem 10.6 — strictly complementary feasible solutions

Open

VanderbeiLP.StrictComp.strictly_complementary_feasible

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

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

and its dual

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

with $A \in \mathbb{R}^{m \times n}$ , $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ . If both the primal and the dual have feasible solutions, then there exist a primal feasible solution $(\bar x, \bar w)$ and a dual feasible solution $(\bar y, \bar z)$ such that

\bar x + \bar z > 0 \qquad \text{and} \qquad \bar y + \bar w > 0,

where $\xi > 0$ means that every component of the vector $\xi$ is strictly positive. Since all four vectors are nonnegative, this says that for each $j$ at least one of $\bar x_j$ , $\bar z_j$ is positive, and for each $i$ at least one of $\bar y_i$ , $\bar w_i$ is positive.

This is the feasible-solution version of strict complementarity; the Strict Complementary Slackness Theorem strengthens it to optimal solutions.

Formalization Note The slacks are determined by the solutions: $\bar w = b - A\bar x$ and $\bar z = A^T \bar y - c$ .

Preamble

import Mathlib
import Definitions.Def_VanderbeiLP_StrictComp_PrimalDualPair

open Matrix

Formal statement

namespace VanderbeiLP.StrictComp

/-- **Vanderbei, Theorem 10.6 (p. 148).** If both the primal (10.9) and the dual (10.10) have
feasible solutions, then there are a primal feasible `x̄` (slack `w̄ = b - Ax̄`) and a dual
feasible `ȳ` (slack `z̄ = Aᵀȳ - c`) with `x̄ + z̄ > 0` and `ȳ + w̄ > 0` componentwise. -/
theorem strictly_complementary_feasible {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (c : Fin n → ℝ)
    (hP : ∃ x : Fin n → ℝ, PrimalFeasible A b x) (hD : ∃ y : Fin m → ℝ, DualFeasible A c y) :
    ∃ (xbar : Fin n → ℝ) (ybar : Fin m → ℝ),
      PrimalFeasible A b xbar ∧ DualFeasible A c ybar ∧
      (∀ j, 0 < xbar j + dualSlack A c ybar j) ∧
      (∀ i, 0 < ybar i + primalSlack A b xbar i) := by sorry

end VanderbeiLP.StrictComp

Source

Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer 2014, p. 148, Theorem 10.6 and footnote 2 (PDF p. 161); Eqs. (10.9)–(10.10), p. 147

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