Duality of Linear Programming


Title: Duality of Linear Programming
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2022-02-03
Abstract: We formalize the weak and strong duality theorems of linear programming. For the strong duality theorem we provide three sufficient preconditions: both the primal problem and the dual problem are satisfiable, the primal problem is satisfiable and bounded, or the dual problem is satisfiable and bounded. The proofs are based on an existing formalization of Farkas' Lemma.
  author  = {René Thiemann},
  title   = {Duality of Linear Programming},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2022,
  note    = {\url{https://isa-afp.org/entries/LP_Duality.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Linear_Inequalities
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.