1. CLRS-Lean
  2. CLRS Fourth Edition
  3. Chapter 29. Linear Programming
  4. 29.1. Standard and Slack Forms
  5. 29.1. Standard-Form Definitions
Imports
import Mathlib

29.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 value cᵀ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 Matrix

A 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 StandardLP

A 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 ⬝ᵥ x
end StandardLPend Chapter29end CLRS