LeanPool.Duality.LinearProgramming

structure ExtendedLP (I : Type u_1) (J : Type u_2) (F : Type u_3) [Field F] [LinearOrder F] [IsStrictOrderedRing F] : Type (max (max u_1 u_2) u_3)

Linear program over F∞ in the standard form (i.e., a system of linear inequalities with nonnegative variables). Variables are of type J. Conditions are indexed by type I. The objective function is intended to be minimized.

• A : Matrix I J F∞

  The left-hand-side matrix.

• b : I → F∞

  The right-hand-side vector.

• c : J → F∞

  The objective function coefficients.

theorem ExtendedLP.ext_iff {I : Type u_1} {J : Type u_2} {F : Type u_3} {inst✝ : Field F} {inst✝¹ : LinearOrder F} {inst✝² : IsStrictOrderedRing F} {x y : ExtendedLP I J F} : x = y ↔ x.A = y.A ∧ x.b = y.b ∧ x.c = y.c

theorem ExtendedLP.ext {I : Type u_1} {J : Type u_2} {F : Type u_3} {inst✝ : Field F} {inst✝¹ : LinearOrder F} {inst✝² : IsStrictOrderedRing F} {x y : ExtendedLP I J F} (A : x.A = y.A) (b : x.b = y.b) (c : x.c = y.c) : x = y

structure ValidELP (I : Type u_1) (J : Type u_2) (F : Type u_3) [Field F] [LinearOrder F] [IsStrictOrderedRing F] extends ExtendedLP I J F : Type (max (max u_1 u_2) u_3)

Extended linear program with properties that are needed for duality theorems.

• A : Matrix I J F∞
• b : I → F∞
• c : J → F∞
• hAi : ¬∃ (i : I), (∃ (j : J), self.A i j = ⊥) ∧ ∃ (j : J), self.A i j = ⊤

  No ⊥ and ⊤ in the same row.

• hAj : ¬∃ (j : J), (∃ (i : I), self.A i j = ⊥) ∧ ∃ (i : I), self.A i j = ⊤

  No ⊥ and ⊤ in the same column.

• hbA : ¬∃ (i : I), (∃ (j : J), self.A i j = ⊥) ∧ self.b i = ⊥

  No ⊥ in the row where the right-hand-side vector has ⊥.

• hcA : ¬∃ (j : J), (∃ (i : I), self.A i j = ⊤) ∧ self.c j = ⊥

  No ⊤ in the column where the objective function has ⊥.

• hAb : ¬∃ (i : I), (∃ (j : J), self.A i j = ⊤) ∧ self.b i = ⊤

  No ⊤ in the row where the right-hand-side vector has ⊤.

• hAc : ¬∃ (j : J), (∃ (i : I), self.A i j = ⊥) ∧ self.c j = ⊤

  No ⊥ in the column where the objective function has ⊤.

def ExtendedLP.IsSolution {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ExtendedLP I J F) (x : J → F≥0) : Prop

A nonnegative vector x is a solution to a linear program P iff its multiplication by matrix A from the left yields a vector whose all entries are less or equal to corresponding entries of the vector b.

Equations

• P.IsSolution x = (P.A ₘ* x ≤ P.b)

def ExtendedLP.Reaches {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ExtendedLP I J F) (r : F∞) : Prop

Linear program P reaches objective value r iff there is a solution x such that, when its entries are elementwise multiplied by the the coefficients c and summed up, the result is the value r.

Equations

• P.Reaches r = ∃ (x : J → F≥0), P.IsSolution x ∧ P.c ᵥ⬝ x = r

def ExtendedLP.IsFeasible {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ExtendedLP I J F) : Prop

Linear program P is feasible iff P reaches a value that is not ⊤.

Equations

• P.IsFeasible = ∃ (p : F∞), P.Reaches p ∧ p ≠ ⊤

def ExtendedLP.IsBoundedBy {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ExtendedLP I J F) (r : F) : Prop

Linear program P is bounded by r iff every value reached by P is greater or equal to r (i.e., P is bounded by r from below).

Equations

• P.IsBoundedBy r = ∀ (p : F∞), P.Reaches p → ↑r ≤ p

def ExtendedLP.IsUnbounded {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ExtendedLP I J F) : Prop

Linear program P is unbounded iff values reached by P have no finite lower bound.

Equations

• P.IsUnbounded = ¬∃ (r : F), P.IsBoundedBy r

noncomputable def ExtendedLP.optimum {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ExtendedLP I J F) : Option F∞

Extended notion of "optimum" of "minimization LP" (the less the better).

Equations

• P.optimum = if ¬P.IsFeasible then some ⊤ else if P.IsUnbounded then some ⊥ else if hr : ∃ (r : F), P.Reaches ↑r ∧ P.IsBoundedBy r then some ↑hr.choose else none

def OppositesOpt {F : Type u_3} [Field F] [LinearOrder F] : Option F∞ → Option F∞ → Prop

OppositesOpt p q essentially says none ≠ p = -q.

Equations

• OppositesOpt (some p) (some q) = (p = -q)
• OppositesOpt x✝¹ x✝ = False

@[reducible, inline]

abbrev ExtendedLP.dualize {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (P : ExtendedLP I J F) : ExtendedLP J I F

Dualize an extended linear program in the standard form. The matrix gets transposed and its values flip signs. The original objective function becomes the new right-hand-side vector. The original right-hand-side vector becomes the new objective function. Both linear programs are intended to be minimized.

Equations

• P.dualize = { A := -P.A.transpose, b := P.c, c := P.b }

def ValidELP.dualize {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (P : ValidELP I J F) : ValidELP J I F

Dualize a valid extended linear program.

Equations

• P.dualize = { toExtendedLP := P.dualize, hAi := ⋯, hAj := ⋯, hbA := ⋯, hcA := ⋯, hAb := ⋯, hAc := ⋯ }

theorem EF.one_smul {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (r : F∞) : 1 • r = r

theorem EF.sub_nonpos_iff {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (r s : F∞) : r + -s ≤ 0 ↔ r ≤ s

theorem EF.vec_sub_nonpos_iff {I : Type u_1} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (u v : I → F∞) : u + -v ≤ 0 ↔ u ≤ v

theorem sumElim_dotWeig_sumElim {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [Fintype I] [Fintype J] (u : I → F∞) (v : J → F∞) (x : I → F≥0) (y : J → F≥0) : Sum.elim u v ᵥ⬝ Sum.elim x y = u ᵥ⬝ x + v ᵥ⬝ y

theorem Matrix.fromRows_mulWeig {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [Fintype J] {I₁ : Type u_4} {I₂ : Type u_5} (M₁ : Matrix I₁ J F∞) (M₂ : Matrix I₂ J F∞) (w : J → F≥0) : M₁.fromRows M₂ ₘ* w = Sum.elim (M₁ ₘ* w) (M₂ ₘ* w)

theorem Matrix.fromCols_mulWeig_sumElim {I : Type u_1} {F : Type u_3} [Field F] [LinearOrder F] {J₁ : Type u_4} {J₂ : Type u_5} [Fintype J₁] [Fintype J₂] (M₁ : Matrix I J₁ F∞) (M₂ : Matrix I J₂ F∞) (w₁ : J₁ → F≥0) (w₂ : J₂ → F≥0) : M₁.fromCols M₂ ₘ* Sum.elim w₁ w₂ = M₁ ₘ* w₁ + M₂ ₘ* w₂

theorem dotWeig_eq_bot {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] {v : J → F∞} {w : J → F≥0} : (∃ (j : J), v j = ⊥) ↔ v ᵥ⬝ w = ⊥

theorem ValidELP.weakDuality_of_no_bot {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype I] [Fintype J] (P : ValidELP I J F) (hb : ¬∃ (i : I), P.b i = ⊥) (hc : ¬∃ (j : J), P.c j = ⊥) {p : F∞} (hP : P.Reaches p) {q : F∞} (hQ : P.dualize.Reaches q) : 0 ≤ p + q

theorem ValidELP.no_bot_of_reaches {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ValidELP I J F) {p : F∞} (hP : P.Reaches p) (i : I) : P.b i ≠ ⊥

theorem ValidELP.weakDuality {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype I] [Fintype J] (P : ValidELP I J F) {p : F∞} (hP : P.Reaches p) {q : F∞} (hQ : P.dualize.Reaches q) : 0 ≤ p + q

theorem eq_zero_of_zero_eq_val {F : Type u_3} [Field F] [LinearOrder F] {k : F≥0} (hk : 0 = ↑k) : k = 0

theorem pos_of_NN_not_zero {F : Type u_3} [Field F] [LinearOrder F] {k : F≥0} (hk : ¬k = 0) : 0 < k

theorem EF.smul_nonpos {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {r : F∞} (hr : r ≤ 0) (k : F≥0) : k • r ≤ 0

theorem EF.smul_lt_smul_left {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {k : F≥0} (hk : 0 < k) (r s : F∞) : k • r < k • s ↔ r < s

theorem EF.smul_le_smul_left {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {k : F≥0} (hk : 0 < k) (r s : F∞) : k • r ≤ k • s ↔ r ≤ s

theorem EF.smul_neg {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {k : F≥0} {r : F∞} (hkr : k = 0 → r ≠ ⊥ ∧ r ≠ ⊤) : k • -r = -(k • r)

theorem EF.pos_smul_neg {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {k : F≥0} (hk : 0 < k) (r : F∞) : k • -r = -(k • r)

theorem EF.smul_smul {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {k : F≥0} (hk : 0 < k) (l : F≥0) (r : F∞) : l • k • r = k • l • r

theorem EF.add_smul {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (k l : F≥0) (r : F∞) : (k + l) • r = k • r + l • r

theorem EF.smul_add {F : Type u_3} [Field F] [LinearOrder F] {k : F≥0} (hk : 0 < k) (r s : F∞) : k • (r + s) = k • r + k • s

theorem EF.mul_smul {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (k l : F≥0) (r : F∞) : (k * l) • r = k • l • r

theorem EF.one_smul_vec {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (v : J → F∞) : 1 • v = v

theorem EF.smul_add_vec {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] {k : F≥0} (hk : 0 < k) (v w : J → F∞) : k • (v + w) = k • v + k • w

theorem EF.mul_smul_vec {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (k l : F≥0) (v : J → F∞) : (k * l) • v = k • l • v

theorem EF.vec_smul_le_smul_left {I : Type u_1} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {k : F≥0} (hk : 0 < k) (u v : I → F∞) : k • u ≤ k • v ↔ u ≤ v

theorem Multiset.sum_neq_EF_top {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {s : Multiset F∞} (hs : ⊤ ∉ s) : s.sum ≠ ⊤

theorem Multiset.smul_EF_sum {F : Type u_3} [Field F] [LinearOrder F] {k : F≥0} (hk : 0 < k) (s : Multiset F∞) : (map (fun (x : F∞) => k • x) s).sum = k • s.sum

theorem Finset.smul_EF_sum {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [Fintype J] {k : F≥0} (hk : 0 < k) (v : J → F∞) : ∑ j : J, k • v j = k • ∑ j : J, v j

theorem zero_dotWeig {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [Fintype J] (w : J → F≥0) : 0 ᵥ⬝ w = 0

theorem dotWeig_add {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (x : J → F∞) (v w : J → F≥0) : x ᵥ⬝ (v + w) = x ᵥ⬝ v + x ᵥ⬝ w

theorem dotWeig_smul {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] {k : F≥0} (hk : 0 < k) (x : J → F∞) (v : J → F≥0) : x ᵥ⬝ k • v = k • (x ᵥ⬝ v)

theorem no_top_dotWeig_nneg {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] {v : J → F∞} (hv : ∀ (j : J), v j ≠ ⊤) (w : J → F≥0) : v ᵥ⬝ w ≠ ⊤

theorem Matrix.EF_neg_zero {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] : -0 = 0

theorem Matrix.EF_neg_neg {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] (M : Matrix I J F∞) : - -M = M

theorem Matrix.zero_mulWeig {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [Fintype J] (v : J → F≥0) : 0 ₘ* v = 0

theorem Matrix.mulWeig_add {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (M : Matrix I J F∞) (v w : J → F≥0) : M ₘ* (v + w) = M ₘ* v + M ₘ* w

theorem Matrix.mulWeig_smul {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] {k : F≥0} (hk : 0 < k) (M : Matrix I J F∞) (v : J → F≥0) : M ₘ* k • v = k • M ₘ* v

theorem ValidELP.dualize_dualize {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (P : ValidELP I J F) : P = P.dualize.dualize

theorem ValidELP.no_bot_of_feasible {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ValidELP I J F) (hP : P.IsFeasible) (i : I) : P.b i ≠ ⊥

theorem ValidELP.isUnbounded_iff {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ValidELP I J F) : P.IsUnbounded ↔ ∀ (r : F), ∃ (p : F∞), P.Reaches p ∧ p < ↑r

theorem ValidELP.unbounded_of_reaches_le {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ValidELP I J F) (hP : ∀ (r : F), ∃ (p : F∞), P.Reaches p ∧ p ≤ ↑r) : P.IsUnbounded

theorem ValidELP.unbounded_of_feasible_of_neg {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] (P : ValidELP I J F) (hP : P.IsFeasible) {x₀ : J → F≥0} (hx₀ : P.c ᵥ⬝ x₀ < 0) (hAx₀ : P.A ₘ* x₀ + 0 • -P.b ≤ 0) : P.IsUnbounded

theorem ValidELP.unbounded_of_feasible_of_infeasible {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] [Fintype I] (P : ValidELP I J F) (hP : P.IsFeasible) (hQ : ¬P.dualize.IsFeasible) : P.IsUnbounded

theorem ValidELP.infeasible_of_unbounded {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] [Fintype I] (P : ValidELP I J F) (hP : P.IsUnbounded) : ¬P.dualize.IsFeasible

The strong duality auxiliary proof is split because the original single proof exceeded the LeanPool 200-line cap. We dispatch on the two cases coming from extendedFarkas and finish each in its own helper.

theorem ValidELP.strongDuality_aux {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] [Fintype I] (P : ValidELP I J F) (hP : P.IsFeasible) (hQ : P.dualize.IsFeasible) : ∃ (p : F) (q : F), P.Reaches ↑p ∧ P.dualize.Reaches ↑q ∧ p + q ≤ 0

theorem ValidELP.strongDuality_of_both_feasible {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] [Fintype I] (P : ValidELP I J F) (hP : P.IsFeasible) (hQ : P.dualize.IsFeasible) : ∃ (r : F), P.Reaches ↑(-r) ∧ P.dualize.Reaches ↑r

theorem ExtendedLP.optimum_unique {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] {P : ExtendedLP I J F} {r s : F} (hPr : P.Reaches ↑r ∧ P.IsBoundedBy r) (hPs : P.Reaches ↑s ∧ P.IsBoundedBy s) : r = s

theorem ExtendedLP.optimum_eq_of_reaches_bounded {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] {P : ExtendedLP I J F} {r : F} (reaches : P.Reaches ↑r) (bounded : P.IsBoundedBy r) : P.optimum = do let a ← some r pure ↑a

theorem oppositesOpt_comm {F : Type u_3} [Field F] [LinearOrder F] (p q : Option F∞) : OppositesOpt p q ↔ OppositesOpt q p

theorem ValidELP.strongDuality_of_prim_feasible {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype I] [Fintype J] (P : ValidELP I J F) (hP : P.IsFeasible) : OppositesOpt P.optimum P.dualize.optimum

theorem ValidELP.optimum_neq_none {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype J] [Finite I] (P : ValidELP I J F) : P.optimum ≠ none

theorem ValidELP.strongDuality_of_dual_feasible {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype I] [Fintype J] (P : ValidELP I J F) (hP : P.dualize.IsFeasible) : OppositesOpt P.optimum P.dualize.optimum

theorem ValidELP.strongDuality {I : Type u_1} {J : Type u_2} {F : Type u_3} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Fintype I] [Fintype J] (P : ValidELP I J F) (hP : P.IsFeasible ∨ P.dualize.IsFeasible) : OppositesOpt P.optimum P.dualize.optimum