29.3 Dual linear programs

For a primal maximization program max cᵀx with Ax ≤ b and x ≥ 0, a dual assignment satisfies y ≥ 0 and Aᵀy ≥ c; its objective is bᵀy.

Main declarations:

StandardLP.IsDualFeasible.
StandardLP.dualObjective.

Downstream layers:

Weak duality is proved in the next module.
Strong duality and complementary slackness are proved by the later Section 29.3 modules together with the initialized solver (online material).

              namespace CLRSnamespace Chapter29open Matrixnamespace StandardLP

A nonnegative vector satisfying c ≤ Aᵀy is dual feasible.

def IsDualFeasible {m n : ℕ} (P : StandardLP m n) (y : Fin m → ℝ) : Prop :=
  IsNonnegative y ∧ ∀ j, P.c j ≤ (P.A.transpose *ᵥ y) j

The dual objective value bᵀy.

def dualObjective {m n : ℕ} (P : StandardLP m n) (y : Fin m → ℝ) : ℝ :=
  P.b ⬝ᵥ y

namespace IsDualFeasible

A dual-feasible assignment is coordinatewise nonnegative.

theorem nonnegative {m n : ℕ} {P : StandardLP m n} {y : Fin m → ℝ}
    (hy : P.IsDualFeasible y) : IsNonnegative y :=
  hy.1

A dual-feasible assignment bounds each primal objective coefficient by the corresponding coordinate of Aᵀy.

theorem coefficient_le {m n : ℕ} {P : StandardLP m n} {y : Fin m → ℝ}
    (hy : P.IsDualFeasible y) :
    ∀ j, P.c j ≤ (P.A.transpose *ᵥ y) j :=
  hy.2

              end IsDualFeasibleend StandardLPend Chapter29end CLRS