Lax Lean Archive

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

Fourier–Motzkin elimination

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

proven

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

    Theorem

    One variable can be eliminated from a finite system of real linear inequalities by nonnegative combinations of its rows. Pair each row with positive coefficient of the eliminated variable with each row with negative coefficient, and retain the rows with zero coefficient. The resulting finite system is feasible exactly when the original system is feasible.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Data.Matrix.Mul
    2import Mathlib.Data.Real.Basic
    3
    4/-!
    5---
    6title: Fourier–Motzkin elimination
    7type: theorem
    8---
    9One variable can be eliminated from a finite system of real linear
    10inequalities by nonnegative combinations of its rows. Pair each row with
    11positive coefficient of the eliminated variable with each row with negative
    12coefficient, and retain the rows with zero coefficient. The resulting finite
    13system is feasible exactly when the original system is feasible.
    14
    15# Formalization notes
    16
    17The variables in this elimination step are unrestricted. Nonnegative
    18variables are represented by additional inequalities when deriving Farkas'
    19lemma. The matrix MM gives the nonnegative row combinations. Its last
    20column in MAMA is zero, and the remaining columns describe the reduced
    21system. This is an algebraic elimination theorem, with no polynomial-time
    22claim: repeated elimination may produce exponentially many inequalities.
    23-/
    24
    25namespace Lax109476.FourierMotzkin
    26
    27/-- Eliminate the last variable using nonnegative row combinations. -/
    28axiom exists_elimination :
    29 ∀ (m : Type) [Fintype m] (n : ℕ)
    30 (A : Matrix m (Fin (n + 1)) ℝ) (b : m → ℝ),
    31 ∃ κ : Type, ∃ _ : Fintype κ, ∃ M : Matrix κ m ℝ,
    32 (∀ i j, 0 ≤ M i j) ∧
    33 (∀ i, (M * A) i (Fin.last n) = 0) ∧
    34 ((∃ x : Fin (n + 1) → ℝ, A.mulVec x ≤ b) ↔
    35 ∃ x' : Fin n → ℝ,
    36 (M * (A.submatrix id Fin.castSucc)).mulVec x' ≤ M.mulVec b)
    37
    38end Lax109476.FourierMotzkin
    39
    Show Proof
    Formalization notes

    The variables in this elimination step are unrestricted. Nonnegative variables are represented by additional inequalities when deriving Farkas' lemma. The matrix MM gives the nonnegative row combinations. Its last column in MAMA is zero, and the remaining columns describe the reduced system. This is an algebraic elimination theorem, with no polynomial-time claim: repeated elimination may produce exponentially many inequalities.

    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…