Linear programming

TheoremStrong linear programming duality#✓fully proved

Let \(A\) be a real \(m \times n\) matrix, and let \(b \in \mathbb{R}^m\) and \(c \in \mathbb{R}^n\); inequalities between vectors are componentwise. Suppose some \(x \in \mathbb{R}^n\) satisfies \(x \ge 0\) and \(Ax \le b\), and that \(c \cdot x\) is bounded above over all such \(x\). Then there exist \(x \in \mathbb{R}^n\) and \(y \in \mathbb{R}^m\) with \(x \ge 0\), \(Ax \le b\), \(y \ge 0\), \(A^{\mathsf{T}} y \ge c\) and \(c \cdot x = b \cdot y\).

By weak duality, such \(x\) and \(y\) are optimal solutions of the primal problem of maximizing \(c \cdot x\) subject to \(x \ge 0\), \(Ax \le b\) and of the dual problem of minimizing \(b \cdot y\) subject to \(y \ge 0\), \(A^{\mathsf{T}} y \ge c\).

Informal source: George B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963, strong duality theorem.

theorem strong_linear_programming_duality {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ)
    (hfeas : ∃ x : Fin n → ℝ, (∀ i, 0 ≤ x i) ∧ ∀ j, (A.mulVec x) j ≤ b j)
    (hbdd : ∃ M : ℝ, ∀ x : Fin n → ℝ,
      (∀ i, 0 ≤ x i) → (∀ j, (A.mulVec x) j ≤ b j) → c ⬝ᵥ x ≤ M) :
    ∃ x : Fin n → ℝ, ∃ y : Fin m → ℝ,
      (∀ i, 0 ≤ x i) ∧ (∀ j, (A.mulVec x) j ≤ b j) ∧
      (∀ j, 0 ≤ y j) ∧ (∀ i, c i ≤ (A.transpose.mulVec y) i) ∧
      c ⬝ᵥ x = b ⬝ᵥ y

Used by 1

Used byStrong duality for flux balance analysis

StructureLinear program#✓fully proved

A linear program in standard inequality form with \(m\) variables and \(n\) constraints is given by an objective vector \(c \in \mathbb{R}^m\), a right-hand side \(b \in \mathbb{R}^n\) and an \(n \times m\) real constraint matrix \(A\); it stands for the problem of maximising \(c \cdot x\) over \(x \in \mathbb{R}^m\) subject to \(A x \le b\) and \(x \ge 0\).

structure LinearProgram (m n : ℕ) where
  /-- Coefficient vector of the objective `c · x`. -/
  c : Fin m → ℝ
  /-- Right-hand side of the inequality constraints `A x ≤ b`. -/
  b : Fin n → ℝ
  /-- Constraint matrix. -/
  A : Matrix (Fin n) (Fin m) ℝ

Used by 4

Used byFeasible region of a linear program · Maximum principle for linear programming · Objective function of a linear program · Optimal vertices of linear programs

DefinitionFeasible region of a linear program#✓fully proved

The feasible region of a linear program with \(m\) variables, constraint matrix \(A\) and right-hand side \(b\) is the set of vectors \(x \in \mathbb{R}^m\) with \(A x \le b\) and \(x \ge 0\), both inequalities holding componentwise. It is a convex polyhedron in \(\mathbb{R}^m\).

def feasible (lp : LinearProgram m n) : Set (Fin m → ℝ) :=
  {x | lp.A *ᵥ x ≤ lp.b ∧ 0 ≤ x}

Uses 1 · Used by 2

Statement usesLinear program

Used byMaximum principle for linear programming · Optimal vertices of linear programs

DefinitionObjective function of a linear program#✓fully proved

The objective function of a linear program with \(m\) variables and objective vector \(c \in \mathbb{R}^m\) is the map \(f \colon \mathbb{R}^m \to \mathbb{R}\) given by \(f(x) = c \cdot x = \sum_i c_i x_i\).

def objective (lp : LinearProgram m n) (x : Fin m → ℝ) : ℝ :=
  lp.c ⬝ᵥ x

Uses 1 · Used by 2

Statement usesLinear program

Used byMaximum principle for linear programming · Optimal vertices of linear programs

TheoremMaximum principle for linear programming#●ready to prove

Consider a linear program with \(m\) variables and objective vector \(c \in \mathbb{R}^m\), let \(P \subseteq \mathbb{R}^m\) be its feasible region and \(f(x) = c \cdot x\) its objective function, and let \(x \in P\) be a local maximiser of \(f\) on \(P\), that is, \(f(y) \le f(x)\) for all \(y \in P\) in some neighbourhood of \(x\). Then \(x\) is a global maximiser of \(f\) on \(P\), and if \(c \ne 0\) then \(x\) lies on the topological boundary of \(P\) in \(\mathbb{R}^m\).

public theorem_wanted lp_maximum_principle {m n : ℕ} (lp : LinearProgram m n)
    (x : Fin m → ℝ) (_hx : x ∈ lp.feasible)
    (_hlocal : IsLocalMaxOn lp.objective lp.feasible x) :
    IsMaxOn lp.objective lp.feasible x ∧
      (lp.c ≠ 0 → x ∈ frontier lp.feasible)

Sources

• G. B. Dantzig (1947), simplex algorithm. Listed as §101 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem lp_maximum_principle of the lean-eval benchmark.

Uses 3

Statement usesLinear program · Feasible region of a linear program · Objective function of a linear program

TheoremOptimal vertices of linear programs#●ready to prove

Consider a linear program with \(m\) variables and objective vector \(c \in \mathbb{R}^m\), and let \(P \subseteq \mathbb{R}^m\) be its feasible region and \(f(x) = c \cdot x\) its objective function. If \(P\) is nonempty and bounded, then some \(x \in P\) maximises \(f\) on \(P\) and is an extreme point of \(P\), that is, \(x\) does not lie in the open segment between two distinct points of \(P\).

public theorem_wanted simplex_algorithm {m n : ℕ} (lp : LinearProgram m n)
    (_hfeas : lp.feasible.Nonempty) (_hbdd : Bornology.IsBounded lp.feasible) :
    ∃ x ∈ lp.feasible, IsMaxOn lp.objective lp.feasible x ∧
      x ∈ Set.extremePoints ℝ lp.feasible

Sources

• G. B. Dantzig (1947), simplex algorithm. Listed as §101 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem lp_maximum_principle of the lean-eval benchmark.

Uses 3

Statement usesLinear program · Feasible region of a linear program · Objective function of a linear program

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.