Lax Lean Archive

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

Farkas' lemma

Lax109476.FarkasLemma · concepts/Lax109476/FarkasLemma.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

    If Ax≤bAx\le b, x≥0x\ge0 has no solution, there is a certificate

    y≥0,ATy≥0,bTy<0.y\ge0,\qquad A^T y\ge0,\qquad b^T y<0.

    Together with certificate soundness, this is the alternative between feasibility and a certificate of infeasibility.

    Concept map
    3 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax109476.FarkasCertificate
    2
    3/-!
    4---
    5title: Farkas' lemma
    6type: theorem
    7---
    8If Ax≤bAx\le b, x≥0x\ge0 has no solution, there is a certificate
    9y≥0,ATy≥0,bTy<0.y\ge0,\qquad A^T y\ge0,\qquad b^T y<0.
    10Together with certificate soundness, this is the alternative between
    11feasibility and a certificate of infeasibility.
    12
    13# Formalization notes
    14
    15This is the inequality form of Farkas' lemma. We state the existence
    16direction separately from the elementary soundness argument. Coefficients
    17and witnesses are real; exact rational certificates are treated downstream.
    18-/
    19
    20namespace Lax109476.FarkasLemma
    21
    22open Lax109476.LinearProgram Lax109476.FarkasCertificate
    23
    24/-- Every infeasible real system has nonnegative separating multipliers. -/
    25axiom exists_infeasibility_certificate :
    26 ∀ (m n : ℕ) (P : Program ℝ m n), ¬ IsFeasible P →
    27 ∃ y : Fin m → ℝ, IsInfeasibilityCertificate P y
    28
    29end Lax109476.FarkasLemma
    30
    Show Proof
    Formalization notes

    This is the inequality form of Farkas' lemma. We state the existence direction separately from the elementary soundness argument. Coefficients and witnesses are real; exact rational certificates are treated downstream.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…