The dual of the dual is the primal
ProvedLinearOptimization.lp_dual_dualdualitylinear-programming
(Theorem 4.1) If we transform the dual into an equivalent minimization problem and then form its dual, we obtain a problem equivalent to the original problem.
("The dual of the dual is the primal.")
Preamble
import Definitions.Def_LinearOptimization_DualLP /-- **Bertsimas & Tsitsiklis, Theorem 4.1 (p. 144).** The dual of the dual is the primal: the equivalent-minimization dual operator is an involution on general-form linear programs. -/
Formal statement
theorem LinearOptimization.lp_dual_dual {m n : ℕ} (P : GeneralFormLP m n) :
dualLP (dualLP P) = P := by
sorry
Source
Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 4.1, p. 144
Human review
Confirmed by the mission captain (proposal self-audit).