EconCSLib.Math.LinearProgramming.StrongDuality

Formalises LP strong duality [MFoGT, Section 2.8, Exercise 9] over any linearly ordered field.

For the standard-form LP pair

Primal P: min ⟨c, x⟩ subject to A x ≥ b and x ≥ 0 Dual D: max ⟨u, b⟩ subject to uᵀA ≤ c and u ≥ 0

if the primal is feasible and bounded below by d ∈ 𝕜, there exists a dual-feasible u with ⟨u, b⟩ ≥ d. Combined with weak duality this yields equal primal/dual optima.

Proof strategy

Apply Farkas (#69) to the augmented system that merges A x ≥ b with the non-negativity constraints x ≥ 0. The augmented row index is I ⊕ Fin n: the original I rows are unchanged, and each Fin n row is the unit row x_{j'} ≥ 0. The primal lower-bound hypothesis becomes a Farkas primal bound on the augmented system, and the Farkas certificate decomposes into (u, v) where u : I → 𝕜 is the dual feasible point and v : Fin n → 𝕜 is the slack on the non-negativity constraints (with uᵀA + v = c, hence uᵀA ≤ c).

Blueprint

• docs/knowledge/nodes/core/linear_programming.strong_duality.md

Standard-form primal / dual predicates

def EconCSLib.LinearProgramming.PrimalFeasible {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) : Prop

Primal feasibility: ∃ x, A x ≥ b ∧ x ≥ 0.

Equations

• EconCSLib.LinearProgramming.PrimalFeasible A b = ∃ (x : Fin n → 𝕜), (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) ∧ ∀ (j : Fin n), 0 ≤ x j

def EconCSLib.LinearProgramming.DualFeasible {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} [Fintype I] {n : ℕ} (A : I → Fin n → 𝕜) (c : Fin n → 𝕜) (u : I → 𝕜) : Prop

Dual feasibility of u: u ≥ 0 ∧ uᵀA ≤ c.

Equations

• EconCSLib.LinearProgramming.DualFeasible A c u = ((∀ (i : I), 0 ≤ u i) ∧ ∀ (j : Fin n), ∑ i : I, u i * A i j ≤ c j)

Weak duality

For any primal-feasible x and dual-feasible u, ⟨c, x⟩ ≥ ⟨u, b⟩.

theorem EconCSLib.LinearProgramming.lp_weak_duality {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) {x : Fin n → 𝕜} (hxA : ∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) (hxnn : ∀ (j : Fin n), 0 ≤ x j) {u : I → 𝕜} (hu_du : DualFeasible A c u) : ∑ i : I, u i * b i ≤ ∑ j : Fin n, c j * x j

Augmented system for strong duality

To reduce LP strong duality to Farkas, augment the primal A x ≥ b with unit rows x_{j'} ≥ 0. The augmented row index is I ⊕ Fin n.

@[reducible, inline]

abbrev EconCSLib.LinearProgramming.DualAugRow (I : Type u_3) (n : ℕ) : Type u_3

Augmented row index for the LP-Farkas reduction.

Equations

• EconCSLib.LinearProgramming.DualAugRow I n = (I ⊕ Fin n)

def EconCSLib.LinearProgramming.dualAugA {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin n → 𝕜) : DualAugRow I n → Fin n → 𝕜

Augmented matrix combining A rows with x ≥ 0 unit rows.

Equations

• EconCSLib.LinearProgramming.dualAugA A (Sum.inl i) x✝ = A i x✝
• EconCSLib.LinearProgramming.dualAugA A (Sum.inr j') x✝ = if x✝ = j' then 1 else 0

def EconCSLib.LinearProgramming.dualAugB {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} (b : I → 𝕜) : DualAugRow I n → 𝕜

Augmented RHS.

Equations

• EconCSLib.LinearProgramming.dualAugB b (Sum.inl i) = b i
• EconCSLib.LinearProgramming.dualAugB b (Sum.inr val) = 0

@[simp]

theorem EconCSLib.LinearProgramming.dualAugA_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (i : I) (j : Fin n) : dualAugA A (Sum.inl i) j = A i j

@[simp]

theorem EconCSLib.LinearProgramming.dualAugA_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (j' j : Fin n) : dualAugA A (Sum.inr j') j = if j = j' then 1 else 0

@[simp]

theorem EconCSLib.LinearProgramming.dualAugB_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (b : I → 𝕜) (i : I) : dualAugB b (Sum.inl i) = b i

@[simp]

theorem EconCSLib.LinearProgramming.dualAugB_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (b : I → 𝕜) (j' : Fin n) : dualAugB b (Sum.inr j') = 0

theorem EconCSLib.LinearProgramming.isFeasible_dualAug_iff {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) : LinearAlgebra.IsFeasible (dualAugA A) (dualAugB b) ↔ PrimalFeasible A b

Augmented feasibility is the primal feasibility (with x ≥ 0).

Strong duality

theorem EconCSLib.LinearProgramming.lp_strong_duality {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) (hP_feas : PrimalFeasible A b) (hP_bound : ∀ (x : Fin n → 𝕜), (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) → (∀ (j : Fin n), 0 ≤ x j) → d ≤ ∑ j : Fin n, c j * x j) : ∃ (u : I → 𝕜), DualFeasible A c u ∧ d ≤ ∑ i : I, u i * b i

LP Strong Duality [MFoGT, Section 2.8, Exercise 9]: if the primal LP min ⟨c, x⟩ s.t. A x ≥ b, x ≥ 0 is feasible and bounded below by d, then there exists a dual-feasible u with ⟨u, b⟩ ≥ d.