Theorem 5.1 — Weak Duality Theorem

Proved

VanderbeiLP.StrictComp.weak_duality

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

dualitylinear-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$ ". If $x = (x_1, \dots, x_n)$ is feasible for the primal and $y = (y_1, \dots, y_m)$ is feasible for the dual, then

\sum_{j=1}^n c_j x_j \le \sum_{i=1}^m b_i y_i.

Every dual feasible point therefore certifies an upper bound on the primal objective, and every primal feasible point a lower bound on the dual objective.

Preamble

import Mathlib
import Definitions.Def_VanderbeiLP_StrictComp_PrimalDualPair

open Matrix

Formal statement

namespace VanderbeiLP.StrictComp

/-- **Vanderbei, Theorem 5.1 (p. 56).** Weak duality: if `x` is primal feasible and `y` is
dual feasible, then `Σⱼ cⱼxⱼ ≤ Σᵢ bᵢyᵢ`. -/
theorem weak_duality {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) :
    c ⬝ᵥ x ≤ b ⬝ᵥ y := by sorry

end VanderbeiLP.StrictComp

Source

Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer 2014, p. 56, Theorem 5.1 (PDF p. 72)

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