Imports
import Mathlib29.1 Standard-form linear programs
This module defines the finite real matrix model used by Chapter 29. A
standard-form program maximizes cᵀx subject to Ax ≤ b and
0 ≤ x.
Main declarations:
-
IsNonnegative: pointwise nonnegativity of a finite vector. -
StandardLP: coefficients, bounds, and objective coefficients. -
StandardLP.IsFeasible: primal standard-form feasibility. -
StandardLP.objective: the valuecᵀx.
Downstream layers:
-
Slack-variable equivalence is proved in later Section 29.1 modules.
-
Basic/nonbasic dictionaries and SIMPLEX are developed in Sections 29.3--29.5.
namespace CLRSnamespace Chapter29open MatrixA finite real vector is nonnegative when every coordinate is nonnegative.
def IsNonnegative {n : ℕ} (x : Fin n → ℝ) : Prop :=
∀ j, 0 ≤ x j
A maximization linear program in CLRS standard form:
maximize cᵀx subject to Ax ≤ b and 0 ≤ x.
The constraint coefficient matrix.
The constraint right-hand side.
The objective coefficient vector.
structure StandardLP (m n : ℕ) where A : Matrix (Fin m) (Fin n) ℝ b : Fin m → ℝ c : Fin n → ℝnamespace StandardLPA vector is primal feasible when it is nonnegative and satisfies every row inequality of the standard-form program.
def IsFeasible {m n : ℕ} (P : StandardLP m n) (x : Fin n → ℝ) : Prop :=
IsNonnegative x ∧ ∀ i, (P.A *ᵥ x) i ≤ P.b i
The objective value cᵀx of a standard-form assignment.
def objective {m n : ℕ} (P : StandardLP m n) (x : Fin n → ℝ) : ℝ :=
P.c ⬝ᵥ xend StandardLPend Chapter29end CLRS