Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Linear programs and their duals

Lax109476.LinearProgram · concepts/Lax109476/LinearProgram.lean · lax-109476

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A linear program in inequality form is

    max⁡{cTx:Ax≤b, x≥0}.\max\{c^T x: Ax\le b,\ x\ge0\}.

    Its dual is

    min⁡{bTy:ATy≥c, y≥0}.\min\{b^T y: A^T y\ge c,\ y\ge0\}.

    All vector inequalities are componentwise. A feasible maximization program is bounded above if one finite real number bounds the objective of every feasible point. A primal point is optimal if it is feasible and no feasible point has a larger objective.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Ring.Finset
    2import Mathlib.Data.Real.Basic
    3import Mathlib.Data.Fintype.Basic
    4
    5/-!
    6---
    7title: Linear programs and their duals
    8type: definition
    9---
    10A linear program in inequality form is
    11max⁡{cTx:Ax≤b, x≥0}.\max\{c^T x: Ax\le b,\ x\ge0\}.
    12Its dual is
    13min⁡{bTy:ATy≥c, y≥0}.\min\{b^T y: A^T y\ge c,\ y\ge0\}.
    14All vector inequalities are componentwise. A feasible maximization program
    15is bounded above if one finite real number bounds the objective of every
    16feasible point. A primal point is optimal if it is feasible and no feasible
    17point has a larger objective.
    18
    19# Formalization notes
    20
    21There are `n` variables and `m` inequalities, indexed by `Fin n` and `Fin m`.
    22The coefficient data are shared by real and rational instances. Feasibility
    23and objective formulas are the same in either field. Both dimensions may be
    24zero. No feasibility, boundedness, optimizer, or optimum value is bundled
    25into the input data. Theorems state the necessary hypotheses explicitly.
    26Equality constraints and unrestricted variables can be represented by paired
    27inequalities and differences of nonnegative variables.
    28-/
    29
    30open scoped BigOperators
    31
    32namespace Lax109476.LinearProgram
    33
    34/-- Coefficients of a maximization program with `m` inequalities and `n`
    35nonnegative variables. -/
    36structure Program (K : Type) (m n : ℕ) where
    37 /-- The constraint matrix. -/
    38 A : Fin m → Fin n → K
    39 /-- The upper bounds on the constraint rows. -/
    40 b : Fin m → K
    41 /-- The coefficients of the maximized objective. -/
    42 c : Fin n → K
    43
    44/-- The value of one constraint row at a primal point. -/
    45def rowValue {K : Type} [Ring K] {m n : ℕ} (P : Program K m n)
    46 (x : Fin n → K) (i : Fin m) : K :=
    47 ∑ j, P.A i j * x j
    48
    49/-- One component of the transposed matrix applied to a dual point. -/
    50def columnValue {K : Type} [Ring K] {m n : ℕ} (P : Program K m n)
    51 (y : Fin m → K) (j : Fin n) : K :=
    52 ∑ i, P.A i j * y i
    53
    54/-- The primal objective value. -/
    55def primalValue {K : Type} [Ring K] {m n : ℕ} (P : Program K m n)
    56 (x : Fin n → K) : K :=
    57 ∑ j, P.c j * x j
    58
    59/-- The dual objective value. -/
    60def dualValue {K : Type} [Ring K] {m n : ℕ} (P : Program K m n)
    61 (y : Fin m → K) : K :=
    62 ∑ i, P.b i * y i
    63
    64/-- A nonnegative primal point satisfies all row upper bounds. -/
    65def PrimalFeasible {K : Type} [Ring K] [PartialOrder K] {m n : ℕ}
    66 (P : Program K m n) (x : Fin n → K) : Prop :=
    67 (∀ j, 0 ≤ x j) ∧ ∀ i, rowValue P x i ≤ P.b i
    68
    69/-- A nonnegative dual point dominates every objective coefficient. -/
    70def DualFeasible {K : Type} [Ring K] [PartialOrder K] {m n : ℕ}
    71 (P : Program K m n) (y : Fin m → K) : Prop :=
    72 (∀ i, 0 ≤ y i) ∧ ∀ j, P.c j ≤ columnValue P y j
    73
    74/-- The real primal feasible set is nonempty. -/
    75def IsFeasible {m n : ℕ} (P : Program ℝ m n) : Prop :=
    76 ∃ x, PrimalFeasible P x
    77
    78/-- A finite upper bound holds for every real primal feasible point. -/
    79def IsBoundedAbove {m n : ℕ} (P : Program ℝ m n) : Prop :=
    80 ∃ B : ℝ, ∀ x, PrimalFeasible P x → primalValue P x ≤ B
    81
    82/-- A primal feasible point maximizes the objective over the feasible set. -/
    83def IsPrimalOptimal {K : Type} [Ring K] [PartialOrder K] {m n : ℕ}
    84 (P : Program K m n) (x : Fin n → K) : Prop :=
    85 PrimalFeasible P x ∧ ∀ z, PrimalFeasible P z → primalValue P z ≤ primalValue P x
    86
    87end Lax109476.LinearProgram
    88
    Formalization notes

    There are nn variables and mm inequalities, indexed by FinnFin n and FinmFin m. The coefficient data are shared by real and rational instances. Feasibility and objective formulas are the same in either field. Both dimensions may be zero. No feasibility, boundedness, optimizer, or optimum value is bundled into the input data. Theorems state the necessary hypotheses explicitly. Equality constraints and unrestricted variables can be represented by paired inequalities and differences of nonnegative variables.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…