Lax Lean Archive

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

Optimal dual multipliers

Lax109476.OptimalDualMultipliers · concepts/Lax109476/OptimalDualMultipliers.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 optimal primal point xx of a real linear program has dual feasible multipliers yy whose objective equals cTxc^T x.

    Concept map
    2 concepts
    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: Optimal dual multipliers
    6type: theorem
    7---
    8Every optimal primal point xx of a real linear program has dual feasible
    9multipliers yy whose objective equals cTxc^T x.
    10
    11# Formalization notes
    12
    13This is the multiplier step in strong duality. Farkas' lemma is applied to
    14the system y≥0y\ge0, ATy≥cA^T y\ge c, bTy≤cTxb^T y\le c^T x. If that system
    15were infeasible, its certificate would produce either a better primal
    16point or a direction improving the objective, contradicting optimality.
    17Weak duality turns the final upper-bound inequality into equality.
    18-/
    19
    20namespace Lax109476.OptimalDualMultipliers
    21
    22open Lax109476.LinearProgram
    23
    24/-- An attained primal optimum has a matching feasible dual certificate. -/
    25axiom exists_matching_dual :
    26 ∀ (m n : ℕ) (P : Program ℝ m n) (x : Fin n → ℝ), IsPrimalOptimal P x →
    27 ∃ y : Fin m → ℝ, DualFeasible P y ∧ primalValue P x = dualValue P y
    28
    29end Lax109476.OptimalDualMultipliers
    30
    Show Proof
    Formalization notes

    This is the multiplier step in strong duality. Farkas' lemma is applied to the system y≥0y\ge0, ATy≥cA^T y\ge c, bTy≤cTxb^T y\le c^T x. If that system were infeasible, its certificate would produce either a better primal point or a direction improving the objective, contradicting optimality. Weak duality turns the final upper-bound inequality into equality.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…