Lax Lean Archive

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

Weak duality

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

    Every primal feasible point xx and dual feasible point yy satisfy

    cTx≤bTy.c^T x\le b^T y.

    Thus a dual feasible point certifies an upper bound on the primal optimum. If their objective values agree, both are optimal.

    Concept map
    2 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.LinearProgram
    2
    3/-!
    4---
    5title: Weak duality
    6type: theorem
    7---
    8Every primal feasible point xx and dual feasible point yy satisfy
    9cTx≤bTy.c^T x\le b^T y.
    10Thus a dual feasible point certifies an upper bound on the primal optimum.
    11If their objective values agree, both are optimal.
    12
    13# Formalization notes
    14
    15The statement uses arbitrary real coefficient data and does not require
    16either feasible set to be bounded. The proof is finite sum rearrangement
    17and multiplication of inequalities by nonnegative coordinates.
    18-/
    19
    20namespace Lax109476.WeakDuality
    21
    22open Lax109476.LinearProgram
    23
    24/-- Every primal objective is bounded by every dual objective. -/
    25axiom primalValue_le_dualValue :
    26 ∀ (m n : ℕ) (P : Program ℝ m n) (x : Fin n → ℝ) (y : Fin m → ℝ),
    27 PrimalFeasible P x → DualFeasible P y → primalValue P x ≤ dualValue P y
    28
    29end Lax109476.WeakDuality
    30
    Show Proof
    Formalization notes

    The statement uses arbitrary real coefficient data and does not require either feasible set to be bounded. The proof is finite sum rearrangement and multiplication of inequalities by nonnegative coordinates.

    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…