29.3. Duality

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.Definitions

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

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.WeakDuality

29.3 Weak duality

This module proves CLRS Theorem 29.8. For every primal-feasible x and dual-feasible y, the primal objective is bounded by the dual objective: cᵀx ≤ bᵀy.

The proof follows the CLRS calculation cᵀx ≤ (Aᵀy)ᵀx = yᵀAx ≤ yᵀb.

Main result:

StandardLP.weak_duality: CLRS Theorem 29.8.

Downstream layers:

Later Section 29.3 modules prove strong duality (Theorem 29.9) and complementary slackness (Theorem 29.10).

              namespace CLRSnamespace Chapter29open Matrixnamespace StandardLP

Increasing the left factor of a dot product preserves order when the right factor is coordinatewise nonnegative.

theorem dotProduct_mono_right_of_nonnegative {n : ℕ}
    {a b x : Fin n → ℝ} (hab : ∀ i, a i ≤ b i) (hx : IsNonnegative x) :
    a ⬝ᵥ x ≤ b ⬝ᵥ x := by
  simp only [dotProduct]
  exact Finset.sum_le_sum fun i _ =>
    mul_le_mul_of_nonneg_right (hab i) (hx i)

Increasing the right factor of a dot product preserves order when the left factor is coordinatewise nonnegative.

theorem dotProduct_mono_left_of_nonnegative {n : ℕ}
    {a b y : Fin n → ℝ} (hab : ∀ i, a i ≤ b i) (hy : IsNonnegative y) :
    y ⬝ᵥ a ≤ y ⬝ᵥ b := by
  simp only [dotProduct]
  exact Finset.sum_le_sum fun i _ =>
    mul_le_mul_of_nonneg_left (hab i) (hy i)

Moving a matrix transpose across a finite dot product exchanges the order of summation: (Aᵀy)ᵀx = yᵀ(Ax).

theorem transpose_mulVec_dotProduct {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (y : Fin m → ℝ) (x : Fin n → ℝ) :
    (A.transpose *ᵥ y) ⬝ᵥ x = y ⬝ᵥ (A *ᵥ x) := by
  simp only [dotProduct, Matrix.mulVec, Matrix.transpose_apply]
  simp_rw [Finset.sum_mul, Finset.mul_sum]
  conv_lhs => rw [Finset.sum_comm]
  apply Finset.sum_congr rfl
  intro i _
  apply Finset.sum_congr rfl
  intro j _
  ring

CLRS Theorem 29.8 (weak duality). Every primal-feasible objective value is at most every dual-feasible objective value.

theorem weak_duality {m n : ℕ} (P : StandardLP m n)
    {x : Fin n → ℝ} {y : Fin m → ℝ}
    (hx : P.IsFeasible x) (hy : P.IsDualFeasible y) :
    P.objective x ≤ P.dualObjective y := by
  calc
    P.objective x = P.c ⬝ᵥ x := rfl
    _ ≤ (P.A.transpose *ᵥ y) ⬝ᵥ x :=
      dotProduct_mono_right_of_nonnegative hy.coefficient_le hx.1
    _ = y ⬝ᵥ (P.A *ᵥ x) := transpose_mulVec_dotProduct P.A y x
    _ ≤ y ⬝ᵥ P.b :=
      dotProduct_mono_left_of_nonnegative hx.2 hy.nonnegative
    _ = P.dualObjective y := by
      simp only [dualObjective, dotProduct]
      apply Finset.sum_congr rfl
      intro i _
      ring

              end StandardLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.Optimality

29.3 Primal and dual optimality specifications

These predicates state the terminal contracts used by strong duality, complementary slackness, and the full initialized SIMPLEX solver.

              namespace CLRSnamespace Chapter29namespace StandardLP

A feasible primal assignment dominating every other feasible assignment.

def IsOptimal (P : StandardLP m n) (x : Fin n → ℝ) : Prop :=
  P.IsFeasible x ∧ ∀ z, P.IsFeasible z → P.objective z ≤ P.objective x

A feasible dual assignment no worse than every other dual assignment.

def IsDualOptimal (P : StandardLP m n) (y : Fin m → ℝ) : Prop :=
  P.IsDualFeasible y ∧
    ∀ z, P.IsDualFeasible z → P.dualObjective y ≤ P.dualObjective z

The primal objective exceeds every real bound on feasible assignments.

def IsUnbounded (P : StandardLP m n) : Prop :=
  ∀ M : ℝ, ∃ x, P.IsFeasible x ∧ M < P.objective x

              end StandardLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.ComplementarySlackness

29.3 Complementary slackness

The duality gap splits exactly into primal-slack and dual-slack products. For feasible assignments all products are nonnegative, so equality of the two objectives is equivalent to the textbook complementary-slackness equations.

              namespace CLRSnamespace Chapter29open Matrixopen scoped BigOperatorsnamespace StandardLP

Slack in primal constraint row i.

def primalSlack (P : StandardLP m n) (x : Fin n → ℝ) (i : Fin m) : ℝ :=
  P.b i - (P.A *ᵥ x) i

Slack in dual constraint column j.

def dualSlack (P : StandardLP m n) (y : Fin m → ℝ) (j : Fin n) : ℝ :=
  (P.A.transpose *ᵥ y) j - P.c j

The textbook complementary-slackness equations.

def ComplementarySlackness (P : StandardLP m n)
    (x : Fin n → ℝ) (y : Fin m → ℝ) : Prop :=
  (∀ i, y i * P.primalSlack x i = 0) ∧
    ∀ j, x j * P.dualSlack y j = 0

Exact decomposition of the duality gap into complementary-slackness products.


theorem dualityGap_eq_slackSums (P : StandardLP m n)
    (x : Fin n → ℝ) (y : Fin m → ℝ) :
    P.dualObjective y - P.objective x =
      (∑ i, y i * P.primalSlack x i) +
        ∑ j, x j * P.dualSlack y j := by
  simp only [dualObjective, objective, primalSlack, dualSlack]
  simp_rw [mul_sub]
  rw [Finset.sum_sub_distrib, Finset.sum_sub_distrib]
  change P.b ⬝ᵥ y - P.c ⬝ᵥ x =
    (y ⬝ᵥ P.b - y ⬝ᵥ (P.A *ᵥ x)) +
      (x ⬝ᵥ (P.A.transpose *ᵥ y) - x ⬝ᵥ P.c)
  rw [dotProduct_comm P.b y, dotProduct_comm x (P.A.transpose *ᵥ y),
    dotProduct_comm x P.c, transpose_mulVec_dotProduct]
  ring

For feasible primal and dual assignments, complementary slackness holds exactly when their objective values agree.


theorem complementarySlackness_iff_objective_eq (P : StandardLP m n)
    {x : Fin n → ℝ} {y : Fin m → ℝ}
    (hx : P.IsFeasible x) (hy : P.IsDualFeasible y) :
    P.ComplementarySlackness x y ↔
      P.objective x = P.dualObjective y := by
  have hpnonneg : ∀ i, 0 ≤ y i * P.primalSlack x i := by
    intro i
    exact mul_nonneg (hy.1 i) (sub_nonneg.mpr (hx.2 i))
  have hdnonneg : ∀ j, 0 ≤ x j * P.dualSlack y j := by
    intro j
    exact mul_nonneg (hx.1 j) (sub_nonneg.mpr (hy.2 j))
  constructor
  · rintro ⟨hp, hd⟩
    have hpsum : (∑ i, y i * P.primalSlack x i) = 0 := by
      apply Finset.sum_eq_zero
      intro i _
      exact hp i
    have hdsum : (∑ j, x j * P.dualSlack y j) = 0 := by
      apply Finset.sum_eq_zero
      intro j _
      exact hd j
    have hgap := P.dualityGap_eq_slackSums x y
    rw [hpsum, hdsum, add_zero] at hgap
    linarith
  · intro hobj
    have hgap := P.dualityGap_eq_slackSums x y
    have htotal :
        (∑ i, y i * P.primalSlack x i) +
          ∑ j, x j * P.dualSlack y j = 0 := by
      linarith
    have hpsum_nonneg : 0 ≤ ∑ i, y i * P.primalSlack x i :=
      Finset.sum_nonneg fun i _ => hpnonneg i
    have hdsum_nonneg : 0 ≤ ∑ j, x j * P.dualSlack y j :=
      Finset.sum_nonneg fun j _ => hdnonneg j
    have hpsum : (∑ i, y i * P.primalSlack x i) = 0 := by
      linarith
    have hdsum : (∑ j, x j * P.dualSlack y j) = 0 := by
      linarith
    have hpzero : (fun i => y i * P.primalSlack x i) = 0 :=
      (Fintype.sum_eq_zero_iff_of_nonneg hpnonneg).mp hpsum
    have hdzero : (fun j => x j * P.dualSlack y j) = 0 :=
      (Fintype.sum_eq_zero_iff_of_nonneg hdnonneg).mp hdsum
    exact ⟨fun i => congrFun hpzero i, fun j => congrFun hdzero j⟩

Complementary slackness certifies primal optimality.

theorem optimal_of_complementarySlackness (P : StandardLP m n)
    {x : Fin n → ℝ} {y : Fin m → ℝ}
    (hx : P.IsFeasible x) (hy : P.IsDualFeasible y)
    (hcs : P.ComplementarySlackness x y) : P.IsOptimal x := by
  have heq := (P.complementarySlackness_iff_objective_eq hx hy).1 hcs
  refine ⟨hx, ?_⟩
  intro z hz
  calc
    P.objective z ≤ P.dualObjective y := P.weak_duality hz hy
    _ = P.objective x := heq.symm

Complementary slackness certifies dual optimality.

theorem dualOptimal_of_complementarySlackness (P : StandardLP m n)
    {x : Fin n → ℝ} {y : Fin m → ℝ}
    (hx : P.IsFeasible x) (hy : P.IsDualFeasible y)
    (hcs : P.ComplementarySlackness x y) : P.IsDualOptimal y := by
  have heq := (P.complementarySlackness_iff_objective_eq hx hy).1 hcs
  refine ⟨hy, ?_⟩
  intro z hz
  calc
    P.dualObjective y = P.objective x := heq.symm
    _ ≤ P.dualObjective z := P.weak_duality hx hz

              end StandardLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.TerminalCertificate

29.3 Dual certificates from terminal dictionaries

When every reduced cost is nonpositive, the negated objective coefficients of the original slack variables are the textbook dual variables. Dictionary equivalence proves both dual feasibility and equality of objective values.

              namespace CLRSnamespace Chapter29open Matrixopen scoped BigOperatorsnamespace Dictionary

Nonpositive reduced costs make the stable objective coefficient of every variable nonpositive; basic variables have coefficient zero.

theorem objectiveCoeff_nonpos_of_reducedCosts (D : Dictionary m n)
    (hc : ∀ j, D.c j ≤ 0) (q : LPVar m n) :
    D.objectiveCoeff q ≤ 0 := by
  rcases D.exists_basic_or_nonbasic q with ⟨i, rfl⟩ | ⟨j, rfl⟩
  · simp
  · simpa using hc j

The shadow-price vector read from a terminal dictionary.

def dualCertificate (D : Dictionary m n) : Fin m → ℝ :=
  fun i => -D.objectiveCoeff (.inr i)

The shadow prices of a terminal dictionary form a feasible solution of the dual of the original standard-form program.


theorem dualCertificate_isDualFeasible (P : StandardLP m n)
    (D : Dictionary m n) (hEq : P.initialDictionary.Equivalent D)
    (hc : ∀ j, D.c j ≤ 0) :
    P.IsDualFeasible D.dualCertificate := by
  constructor
  · intro i
    exact neg_nonneg.mpr
      (D.objectiveCoeff_nonpos_of_reducedCosts hc (.inr i))
  · intro j
    have hid := hEq.entering_coefficient_identity j
    have horiginal : D.objectiveCoeff (.inl j) ≤ 0 :=
      D.objectiveCoeff_nonpos_of_reducedCosts hc (.inl j)
    have hsum :
        (P.A.transpose *ᵥ D.dualCertificate) j =
          -(∑ i, D.objectiveCoeff (.inr i) * P.A i j) := by
      change (∑ i, P.A i j * (-D.objectiveCoeff (.inr i))) = _
      rw [← Finset.sum_neg_distrib]
      apply Finset.sum_congr rfl
      intro i _
      ring
    change P.c j = D.objectiveCoeff (.inl j) -
      ∑ i, D.objectiveCoeff (.inr i) * P.A i j at hid
    rw [hsum]
    linarith

The objective of the terminal dual certificate equals the terminal dictionary's objective constant.


theorem dualCertificate_objective_eq_v (P : StandardLP m n)
    (D : Dictionary m n) (hEq : P.initialDictionary.Equivalent D) :
    P.dualObjective D.dualCertificate = D.v := by
  let D₀ := P.initialDictionary
  have hobj := hEq.2 D₀.basicAssignment D₀.basicAssignment_satisfies
  have hsum :
      (∑ q, D.objectiveCoeff q * D₀.basicAssignment q) =
        ∑ i, D.objectiveCoeff (.inr i) * P.b i := by
    rw [D₀.sum_eq_sum_labels, Fintype.sum_sum_type]
    change
      (∑ i, D.objectiveCoeff (D₀.basicVar i) *
          D₀.basicAssignment (D₀.basicVar i)) +
        (∑ j, D.objectiveCoeff (D₀.nonbasicVar j) *
          D₀.basicAssignment (D₀.nonbasicVar j)) = _
    simp only [Dictionary.basicAssignment_basicVar,
      Dictionary.basicAssignment_nonbasicVar, mul_zero,
      Finset.sum_const_zero, add_zero]
    change (∑ i, D.objectiveCoeff (.inr i) * P.b i) = _
    rfl
  have hzero :
      0 = D.v + ∑ i, D.objectiveCoeff (.inr i) * P.b i := by
    calc
      0 = D₀.objectiveRhs D₀.basicAssignment := by
        rw [D₀.objectiveRhs_basicAssignment]
        rfl
      _ = D.objectiveRhs D₀.basicAssignment := hobj
      _ = D.v + ∑ q, D.objectiveCoeff q * D₀.basicAssignment q :=
        D.objectiveRhs_eq_fullSum D₀.basicAssignment
      _ = D.v + ∑ i, D.objectiveCoeff (.inr i) * P.b i := by
        rw [hsum]
  change (∑ i, P.b i * (-D.objectiveCoeff (.inr i))) = D.v
  have hneg :
      (∑ i, P.b i * (-D.objectiveCoeff (.inr i))) =
        -(∑ i, D.objectiveCoeff (.inr i) * P.b i) := by
    rw [← Finset.sum_neg_distrib]
    apply Finset.sum_congr rfl
    intro i _
    ring
  rw [hneg]
  linarith

              end Dictionaryend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.DictionaryBridge

29.3 Bridge from dictionary assignments to the primal program

The initial dictionary uses one stable assignment containing both original and slack variables. This module projects that assignment back to the standard-form primal variables and transports optimality and unboundedness.

              namespace CLRSnamespace Chapter29namespace Dictionary

Original-variable coordinates of a complete dictionary assignment.

def assignmentOriginal (z : LPVar m n → ℝ) : Fin n → ℝ :=
  fun j => z (.inl j)

Slack-variable coordinates of a complete dictionary assignment.

def assignmentSlack (z : LPVar m n → ℝ) : Fin m → ℝ :=
  fun i => z (.inr i)

@[simp] theorem assignmentOriginal_combinedAssignment
    (x : Fin n → ℝ) (s : Fin m → ℝ) :
    assignmentOriginal (StandardLP.combinedAssignment x s) = x := by
  funext j
  rfl

@[simp] theorem assignmentSlack_combinedAssignment
    (x : Fin n → ℝ) (s : Fin m → ℝ) :
    assignmentSlack (StandardLP.combinedAssignment x s) = s := by
  funext i
  rfl

Splitting and recombining a stable assignment is the identity.

theorem combinedAssignment_parts (z : LPVar m n → ℝ) :
    StandardLP.combinedAssignment (assignmentOriginal z)
      (assignmentSlack z) = z := by
  funext q
  cases q <;> rfl

A nonnegative assignment satisfying the initial dictionary projects to a feasible assignment of the original standard-form program.


theorem original_feasible_of_initialDictionary (P : StandardLP m n)
    {z : LPVar m n → ℝ} (hznonneg : IsNonnegativeAssignment z)
    (hzsat : P.initialDictionary.Satisfies z) :
    P.IsFeasible (assignmentOriginal z) := by
  apply StandardLP.feasible_of_slackExtension
  refine ⟨fun j => hznonneg (.inl j), fun i => hznonneg (.inr i), ?_⟩
  apply (P.initialDictionary_satisfies_iff
    (assignmentOriginal z) (assignmentSlack z)).1
  rw [combinedAssignment_parts]
  exact hzsat

On every complete assignment, the initial dictionary objective is the standard-form objective of its original-variable projection.


theorem initialDictionary_objectiveRhs_eq_objective_original
    (P : StandardLP m n) (z : LPVar m n → ℝ) :
    P.initialDictionary.objectiveRhs z =
      P.objective (assignmentOriginal z) := by
  rw [← combinedAssignment_parts z]
  exact P.initialDictionary_objectiveRhs _ _

Dictionary optimality for the initial representation yields primal optimality for the original standard-form program.

theorem initialDictionary_optimal_to_standardLP (P : StandardLP m n)
    {z : LPVar m n → ℝ}
    (hz : P.initialDictionary.IsOptimalAssignment z) :
    P.IsOptimal (assignmentOriginal z) := by
  refine ⟨original_feasible_of_initialDictionary P hz.1 hz.2.1, ?_⟩
  intro x hx
  let w := StandardLP.combinedAssignment x (P.slack x)
  have hwext := P.slackExtension_of_feasible hx
  have hwnonneg : IsNonnegativeAssignment w :=
    (StandardLP.combinedAssignment_nonnegative_iff x (P.slack x)).2
      ⟨hwext.1, hwext.2.1⟩
  have hwsat : P.initialDictionary.Satisfies w :=
    P.initialDictionary_satisfies_of_slackExtension hwext
  have hle := hz.2.2 w hwnonneg hwsat
  calc
    P.objective x = P.initialDictionary.objectiveRhs w := by
      exact (P.initialDictionary_objectiveRhs x (P.slack x)).symm
    _ ≤ P.initialDictionary.objectiveRhs z := hle
    _ = P.objective (assignmentOriginal z) :=
      initialDictionary_objectiveRhs_eq_objective_original P z

Dictionary unboundedness for the initial representation yields unboundedness of the original standard-form program.


theorem initialDictionary_unbounded_to_standardLP (P : StandardLP m n)
    (h : P.initialDictionary.IsUnbounded) : P.IsUnbounded := by
  intro M
  obtain ⟨z, hznonneg, hzsat, hzobj⟩ := h M
  refine ⟨assignmentOriginal z,
    original_feasible_of_initialDictionary P hznonneg hzsat, ?_⟩
  rw [← initialDictionary_objectiveRhs_eq_objective_original P z]
  exact hzobj

              end Dictionaryend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.StrongDuality

29.3 Strong duality from finite SIMPLEX

For an initially basic-feasible standard-form program, finite Bland-SIMPLEX either produces an unbounded primal ray or a terminal dictionary. In the terminal case its basic assignment and shadow prices are primal/dual optimal and have the same objective value.

              namespace CLRSnamespace Chapter29namespace StandardLP

Strong duality from any basic-feasible dictionary equivalent to the program's initial dictionary.


theorem strongDuality_or_unbounded_of_equivalent_isBasicFeasible
    (P : StandardLP m n) (D : Dictionary m n)
    (hEq₀ : P.initialDictionary.Equivalent D)
    (hD : D.IsBasicFeasible) :
    P.IsUnbounded ∨
      ∃ x y, P.IsOptimal x ∧ P.IsDualOptimal y ∧
        P.objective x = P.dualObjective y := by
  let fuel := Dictionary.basisCount m n
  cases hrun : D.simplexRun fuel with
  | optimal terminal hc =>
      have hEq : P.initialDictionary.Equivalent terminal :=
        hEq₀.trans (by
          simpa [hrun, Dictionary.SimplexRunResult.terminalDictionary] using
            D.simplexRun_equivalent fuel)
      have hterminal : terminal.IsBasicFeasible := by
        simpa [hrun, Dictionary.SimplexRunResult.terminalDictionary] using
          D.simplexRun_isBasicFeasible fuel hD
      have hdictOptimal :
          P.initialDictionary.IsOptimalAssignment terminal.basicAssignment :=
        hEq.isOptimalAssignment
          (terminal.basicAssignment_optimal_of_reducedCosts_nonpos
            hterminal hc)
      let x := Dictionary.assignmentOriginal terminal.basicAssignment
      let y := terminal.dualCertificate
      have hx : P.IsOptimal x := by
        exact Dictionary.initialDictionary_optimal_to_standardLP P
          hdictOptimal
      have hyfeasible : P.IsDualFeasible y := by
        exact terminal.dualCertificate_isDualFeasible P hEq hc
      have hterminalSatD₀ :
          P.initialDictionary.Satisfies terminal.basicAssignment :=
        (hEq.1 terminal.basicAssignment).2
          terminal.basicAssignment_satisfies
      have hprimalValue : P.objective x = terminal.v := by
        calc
          P.objective x =
              P.initialDictionary.objectiveRhs terminal.basicAssignment :=
            (Dictionary.initialDictionary_objectiveRhs_eq_objective_original
              P terminal.basicAssignment).symm
          _ = terminal.objectiveRhs terminal.basicAssignment :=
            hEq.2 terminal.basicAssignment hterminalSatD₀
          _ = terminal.v := terminal.objectiveRhs_basicAssignment
      have hdualValue : P.dualObjective y = terminal.v :=
        terminal.dualCertificate_objective_eq_v P hEq
      have hvalue : P.objective x = P.dualObjective y :=
        hprimalValue.trans hdualValue.symm
      have hcs : P.ComplementarySlackness x y :=
        (P.complementarySlackness_iff_objective_eq hx.1 hyfeasible).2 hvalue
      have hy : P.IsDualOptimal y :=
        P.dualOptimal_of_complementarySlackness hx.1 hyfeasible hcs
      exact Or.inr ⟨x, y, hx, hy, hvalue⟩
  | unbounded terminal entering he ha =>
      have hEq : P.initialDictionary.Equivalent terminal :=
        hEq₀.trans (by
          simpa [hrun, Dictionary.SimplexRunResult.terminalDictionary] using
            D.simplexRun_equivalent fuel)
      have hterminal : terminal.IsBasicFeasible := by
        simpa [hrun, Dictionary.SimplexRunResult.terminalDictionary] using
          D.simplexRun_isBasicFeasible fuel hD
      have hunbounded : P.initialDictionary.IsUnbounded :=
        hEq.isUnbounded
          (terminal.unbounded_of_entering_column hterminal entering he.1 ha)
      exact Or.inl
        (Dictionary.initialDictionary_unbounded_to_standardLP P hunbounded)
  | exhausted terminal =>
      exact False.elim (D.simplexRun_basisCount_not_exhausted hD (by
        simp [fuel, hrun, Dictionary.SimplexRunResult.IsExhausted]))

Strong duality, with the alternative unbounded outcome made explicit, for programs whose initial slack dictionary is basic feasible.

theorem strongDuality_or_unbounded_of_initialDictionary_isBasicFeasible
    (P : StandardLP m n) (hP : P.initialDictionary.IsBasicFeasible) :
    P.IsUnbounded ∨
      ∃ x y, P.IsOptimal x ∧ P.IsDualOptimal y ∧
        P.objective x = P.dualObjective y :=
  P.strongDuality_or_unbounded_of_equivalent_isBasicFeasible
    P.initialDictionary (Dictionary.Equivalent.refl _) hP

If the primal is not unbounded, finite SIMPLEX yields primal and dual optima with equal objective values.

theorem strongDuality_of_initialDictionary_isBasicFeasible
    (P : StandardLP m n) (hP : P.initialDictionary.IsBasicFeasible)
    (hbounded : ¬P.IsUnbounded) :
    ∃ x y, P.IsOptimal x ∧ P.IsDualOptimal y ∧
      P.objective x = P.dualObjective y := by
  rcases P.strongDuality_or_unbounded_of_initialDictionary_isBasicFeasible hP
      with hunbounded | hopt
  · exact False.elim (hbounded hunbounded)
  · exact hopt

              end StandardLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.ComplementarySlacknessTheorem

29.3 The complementary-slackness theorem

This closes the converse direction of the textbook theorem: for feasible primal and dual assignments, simultaneous optimality is equivalent to the complementary-slackness equations.

              namespace CLRSnamespace Chapter29namespace StandardLP

Any dual-feasible assignment gives a finite upper bound on all primal feasible objective values.

theorem not_isUnbounded_of_isDualFeasible (P : StandardLP m n)
    {y : Fin m → ℝ} (hy : P.IsDualFeasible y) : ¬P.IsUnbounded := by
  intro hunbounded
  obtain ⟨x, hx, hlarge⟩ := hunbounded (P.dualObjective y)
  have hweak := P.weak_duality hx hy
  linarith

CLRS complementary-slackness theorem for an initially basic-feasible program: feasible primal and dual assignments are both optimal exactly when their complementary products vanish.


theorem complementarySlackness_iff_optimal_of_initialDictionary_isBasicFeasible
    (P : StandardLP m n) (hP : P.initialDictionary.IsBasicFeasible)
    {x : Fin n → ℝ} {y : Fin m → ℝ}
    (hx : P.IsFeasible x) (hy : P.IsDualFeasible y) :
    P.ComplementarySlackness x y ↔
      P.IsOptimal x ∧ P.IsDualOptimal y := by
  constructor
  · intro hcs
    exact ⟨P.optimal_of_complementarySlackness hx hy hcs,
      P.dualOptimal_of_complementarySlackness hx hy hcs⟩
  · rintro ⟨hxoptimal, hyoptimal⟩
    obtain ⟨x₀, y₀, hx₀, hy₀, hvalue₀⟩ :=
      P.strongDuality_of_initialDictionary_isBasicFeasible hP
        (P.not_isUnbounded_of_isDualFeasible hy)
    have hprimal : P.objective x = P.objective x₀ :=
      le_antisymm (hx₀.2 x hx) (hxoptimal.2 x₀ hx₀.1)
    have hdual : P.dualObjective y = P.dualObjective y₀ :=
      le_antisymm (hyoptimal.2 y₀ hy₀.1) (hy₀.2 y hy)
    have hvalue : P.objective x = P.dualObjective y := by
      calc
        P.objective x = P.objective x₀ := hprimal
        _ = P.dualObjective y₀ := hvalue₀
        _ = P.dualObjective y := hdual.symm
    exact (P.complementarySlackness_iff_objective_eq hx hy).2 hvalue

              end StandardLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.GeneralStrongDuality

29.3 General strong duality

Phase II supplies the equivalent basic-feasible dictionary required by the finite-SIMPLEX strong-duality proof. Projecting both primal and dual locked coordinates yields the unrestricted textbook theorems for the original LP.

This module is the canonical fourth-edition owner of the general (no initial-basis hypothesis) strong-duality and complementary-slackness theorems. The phase-I/II initialization machinery it builds on remains online material (reachable through CLRSLean.OnlineMaterial); only the resulting duality declarations live here.

              namespace CLRSnamespace Chapter29namespace StandardLP

Every feasible standard-form program is either unbounded or has primal and dual optima with equal values.


theorem strongDuality_or_unbounded_of_feasible (P : StandardLP m n)
    (hfeasible : ∃ x, P.IsFeasible x) :
    P.IsUnbounded ∨
      ∃ x y, P.IsOptimal x ∧ P.IsDualOptimal y ∧
        P.objective x = P.dualObjective y := by
  have hlocked :=
    P.lockedAuxiliary.strongDuality_or_unbounded_of_equivalent_isBasicFeasible
      P.phaseTwoStart P.phaseTwoStart_equivalent_lockedAuxiliary
      (P.phaseTwoStart_isBasicFeasible hfeasible)
  rcases hlocked with hunbounded | ⟨z, y, hz, hy, hvalue⟩
  · exact Or.inl (P.lockedAuxiliary_unbounded_to_original hunbounded)
  · let x₀ := auxiliaryTail z
    let y₀ := lockedDualTail y
    have hx₀ : P.IsOptimal x₀ :=
      P.lockedAuxiliary_optimal_to_original hz
    have hy₀feasible : P.IsDualFeasible y₀ :=
      P.lockedAuxiliary_dualFeasible_to_original hy.1
    have hvalue₀ : P.objective x₀ = P.dualObjective y₀ := by
      calc
        P.objective x₀ = P.lockedAuxiliary.objective z :=
          (P.lockedAuxiliary_objective z).symm
        _ = P.lockedAuxiliary.dualObjective y := hvalue
        _ = P.dualObjective y₀ := P.lockedAuxiliary_dualObjective y
    have hy₀ : P.IsDualOptimal y₀ := by
      refine ⟨hy₀feasible, ?_⟩
      intro y' hy'
      calc
        P.dualObjective y₀ = P.objective x₀ := hvalue₀.symm
        _ ≤ P.dualObjective y' := P.weak_duality hx₀.1 hy'
    exact Or.inr ⟨x₀, y₀, hx₀, hy₀, hvalue₀⟩

General strong duality: a feasible, bounded primal program has primal and dual optima with equal objective values.

theorem strongDuality (P : StandardLP m n)
    (hfeasible : ∃ x, P.IsFeasible x) (hbounded : ¬P.IsUnbounded) :
    ∃ x y, P.IsOptimal x ∧ P.IsDualOptimal y ∧
      P.objective x = P.dualObjective y := by
  rcases P.strongDuality_or_unbounded_of_feasible hfeasible with
    hunbounded | hopt
  · exact False.elim (hbounded hunbounded)
  · exact hopt

An attained primal optimum rules out primal unboundedness.

theorem not_isUnbounded_of_isOptimal (P : StandardLP m n)
    {x : Fin n → ℝ} (hx : P.IsOptimal x) : ¬P.IsUnbounded := by
  intro hunbounded
  obtain ⟨z, hz, hlarge⟩ := hunbounded (P.objective x)
  exact (not_lt_of_ge (hx.2 z hz)) hlarge

Textbook strong-duality form for a given attained primal optimum.

theorem strongDuality_of_isOptimal (P : StandardLP m n)
    {x : Fin n → ℝ} (hx : P.IsOptimal x) :
    ∃ y, P.IsDualOptimal y ∧ P.objective x = P.dualObjective y := by
  obtain ⟨x₀, y, hx₀, hy, hvalue₀⟩ :=
    P.strongDuality ⟨x, hx.1⟩ (P.not_isUnbounded_of_isOptimal hx)
  have hprimal : P.objective x = P.objective x₀ :=
    le_antisymm (hx₀.2 x hx.1) (hx.2 x₀ hx₀.1)
  exact ⟨y, hy, hprimal.trans hvalue₀⟩

CLRS complementary-slackness theorem without an initial-basis hypothesis: feasible primal and dual assignments are simultaneously optimal exactly when all complementary products vanish.

theorem complementarySlackness_iff_optimal (P : StandardLP m n)
    {x : Fin n → ℝ} {y : Fin m → ℝ}
    (hx : P.IsFeasible x) (hy : P.IsDualFeasible y) :
    P.ComplementarySlackness x y ↔
      P.IsOptimal x ∧ P.IsDualOptimal y := by
  constructor
  · intro hcs
    exact ⟨P.optimal_of_complementarySlackness hx hy hcs,
      P.dualOptimal_of_complementarySlackness hx hy hcs⟩
  · rintro ⟨hxoptimal, hyoptimal⟩
    obtain ⟨y₀, hy₀, hvalue₀⟩ := P.strongDuality_of_isOptimal hxoptimal
    have hdual : P.dualObjective y = P.dualObjective y₀ :=
      le_antisymm (hyoptimal.2 y₀ hy₀.1) (hy₀.2 y hy)
    have hvalue : P.objective x = P.dualObjective y :=
      hvalue₀.trans hdual.symm
    exact (P.complementarySlackness_iff_objective_eq hx hy).2 hvalue

              end StandardLPend Chapter29end CLRS

Implementation details

Definitions and proofs