We prove properties of "normal" linear programs as a corollary of properties of extended linear programs. The only exception is the weak duality theorem, which is proved separately, to allow weaker assumptions.

structure StandardLP (I : Type u_1) (J : Type u_2) (R : Type u_3) : Type (max (max u_1 u_2) u_3)

Linear program in the standard form. Variables are of type J. Conditions are indexed by type I. The objective function is intended to be minimized.

• A : Matrix I J R

  The left-hand-side matrix

• b : I → R

  The right-hand-side vector

• c : J → R

  The objective function coefficients

def coeNN {I : Type u_1} {R : Type u_2} [Zero R] [LE R] : (I → R≥0) → I → R

Coerce a vector of nonnegative values into a vector of the underlying ring.

Equations

• ↑x✝ = Subtype.val ∘ x✝

@[implicit_reducible]

instance instCoeForallNNegForall {I : Type u_1} {R : Type u_2} [Zero R] [LE R] : Coe (I → R≥0) (I → R)

Equations

• instCoeForallNNegForall = { coe := coeNN }

def StandardLP.IsSolution {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Semiring R] [PartialOrder R] (P : StandardLP I J R) (x : J → R≥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.mulVec ↑x ≤ P.b)

def StandardLP.Reaches {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Semiring R] [PartialOrder R] (P : StandardLP I J R) (r : R) : 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 → R≥0), P.IsSolution x ∧ P.c ⬝ᵥ ↑x = r

def StandardLP.IsFeasible {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Semiring R] [PartialOrder R] (P : StandardLP I J R) : Prop

Linear program P is feasible iff there exists a solution to P.

Equations

• P.IsFeasible = ∃ (r : R), P.Reaches r

def StandardLP.IsBoundedBy {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Semiring R] [PartialOrder R] (P : StandardLP I J R) (r : R) : 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 : R), P.Reaches p → r ≤ p

def StandardLP.IsUnbounded {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Semiring R] [PartialOrder R] (P : StandardLP I J R) : Prop

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

Equations

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

def StandardLP.dualize {I : Type u_1} {R : Type u_2} {J : Type u_3} [Ring R] (P : StandardLP I J R) : StandardLP J I R

Dualize a 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 }

theorem Matrix.transpose_mulVec_dotProduct {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Fintype I] [CommSemiring R] (M : Matrix I J R) (v : I → R) (w : J → R) : M.transpose.mulVec v ⬝ᵥ w = M.mulVec w ⬝ᵥ v

theorem StandardLP.weakDuality {I : Type u_1} {R : Type u_2} {J : Type u_3} [Fintype J] [Fintype I] [CommRing R] [PartialOrder R] [IsOrderedRing R] {P : StandardLP I J R} {p : R} (hP : P.Reaches p) {q : R} (hQ : P.dualize.Reaches q) : 0 ≤ p + q

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

The "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 : R), P.Reaches r ∧ P.IsBoundedBy r then some ↑hr.choose else none

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

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