Lax Lean Archive

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

Complementary slackness

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

    For a primal feasible point xx and a dual feasible point yy, the objective values agree if and only if

    yi(bi−(Ax)i)=0for every i,y_i(b_i-(Ax)_i)=0\quad\text{for every }i,xj((ATy)j−cj)=0for every j.x_j((A^T y)_j-c_j)=0\quad\text{for every }j.

    Thus matching feasible certificates can equivalently be checked by these complementarity conditions.

    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: Complementary slackness
    6type: theorem
    7---
    8For a primal feasible point xx and a dual feasible point yy, the objective
    9values agree if and only if
    10yi(bi−(Ax)i)=0for every i,y_i(b_i-(Ax)_i)=0\quad\text{for every }i,
    11xj((ATy)j−cj)=0for every j.x_j((A^T y)_j-c_j)=0\quad\text{for every }j.
    12Thus matching feasible certificates can equivalently be checked by these
    13complementarity conditions.
    14
    15# Formalization notes
    16
    17Feasibility makes every displayed product nonnegative. The difference of
    18the objectives is the sum of all these products, so it vanishes exactly
    19when each product vanishes. This identity requires no existence theorem.
    20-/
    21
    22namespace Lax109476.ComplementarySlackness
    23
    24open Lax109476.LinearProgram
    25
    26/-- Matching feasible objectives are equivalent to coordinatewise complementarity. -/
    27axiom matching_iff_slackness :
    28 ∀ (m n : ℕ) (P : Program ℝ m n) (x : Fin n → ℝ) (y : Fin m → ℝ),
    29 PrimalFeasible P x → DualFeasible P y →
    30 (primalValue P x = dualValue P y ↔
    31 (∀ i, y i * (P.b i - rowValue P x i) = 0) ∧
    32 (∀ j, x j * (columnValue P y j - P.c j) = 0))
    33
    34end Lax109476.ComplementarySlackness
    35
    Show Proof
    Formalization notes

    Feasibility makes every displayed product nonnegative. The difference of the objectives is the sum of all these products, so it vanishes exactly when each product vanishes. This identity requires no existence theorem.

    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…