Lax Lean Archive

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

Certificates of infeasibility

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

    For the system Ax≤bAx\le b, x≥0x\ge0, an infeasibility certificate is a vector yy satisfying

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

    Such a vector is incompatible with primal feasibility: multiplying the constraints by yy would give 0≤yTAx≤yTb<00\le y^T Ax\le y^T b<0.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax109476.LinearProgram
    2
    3/-!
    4---
    5title: Certificates of infeasibility
    6type: definition
    7---
    8For the system Ax≤bAx\le b, x≥0x\ge0, an infeasibility certificate is a vector
    9yy satisfying
    10y≥0,ATy≥0,bTy<0.y\ge0,\qquad A^T y\ge0,\qquad b^T y<0.
    11Such a vector is incompatible with primal feasibility: multiplying the
    12constraints by yy would give 0≤yTAx≤yTb<00\le y^T Ax\le y^T b<0.
    13
    14# Formalization notes
    15
    16The certificate is defined over the same coefficient field as the program,
    17so rational certificates can be checked exactly. The objective coefficients
    18are irrelevant to this certificate. Existence of a certificate for every
    19infeasible real system is the separate Farkas theorem.
    20-/
    21
    22namespace Lax109476.FarkasCertificate
    23
    24open Lax109476.LinearProgram
    25
    26/-- Nonnegative row multipliers certify an impossible negative upper bound. -/
    27def IsInfeasibilityCertificate {K : Type} [Ring K] [PartialOrder K] {m n : ℕ}
    28 (P : Program K m n) (y : Fin m → K) : Prop :=
    29 (∀ i, 0 ≤ y i) ∧ (∀ j, 0 ≤ columnValue P y j) ∧ dualValue P y < 0
    30
    31end Lax109476.FarkasCertificate
    32
    Formalization notes

    The certificate is defined over the same coefficient field as the program, so rational certificates can be checked exactly. The objective coefficients are irrelevant to this certificate. Existence of a certificate for every infeasible real system is the separate Farkas theorem.

    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…