Lax Lean Archive

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

Certificates of unboundedness

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

    An improving recession direction satisfies

    d≥0,Ad≤0,cTd>0.d\ge0,\qquad Ad\le0,\qquad c^T d>0.

    Together with any primal feasible point xx, it certifies unboundedness: x+tdx+td is feasible for every t≥0t\ge0 and its objective tends to infinity.

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

    Lean source view on GitHub

    1import Lax109476.LinearProgram
    2
    3/-!
    4---
    5title: Certificates of unboundedness
    6type: definition
    7---
    8An improving recession direction satisfies
    9d≥0,Ad≤0,cTd>0.d\ge0,\qquad Ad\le0,\qquad c^T d>0.
    10Together with any primal feasible point xx, it certifies unboundedness:
    11x+tdx+td is feasible for every t≥0t\ge0 and its objective tends to infinity.
    12
    13# Formalization notes
    14
    15A direction alone does not certify that the primal is unbounded: the
    16feasible set could be empty. Certificates therefore include a feasible
    17base point as well as the direction.
    18-/
    19
    20namespace Lax109476.RecessionDirection
    21
    22open Lax109476.LinearProgram
    23
    24/-- A nonnegative direction preserves every upper constraint and improves
    25the maximized objective. -/
    26def IsImprovingDirection {K : Type} [Ring K] [PartialOrder K] {m n : ℕ}
    27 (P : Program K m n) (d : Fin n → K) : Prop :=
    28 (∀ j, 0 ≤ d j) ∧ (∀ i, rowValue P d i ≤ 0) ∧ 0 < primalValue P d
    29
    30end Lax109476.RecessionDirection
    31
    Formalization notes

    A direction alone does not certify that the primal is unbounded: the feasible set could be empty. Certificates therefore include a feasible base point as well as the direction.

    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…