CLRS-Lean
CLRS Fourth Edition
Chapter 29. Linear Programming
29.4. Duality

Imports

import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.Definitions
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.WeakDuality
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.Optimality
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.ComplementarySlackness
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.TerminalCertificate
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.DictionaryBridge
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.StrongDuality
import CLRSLean.FourthEdition.Chapter_29.Section_29_3_Duality.ComplementarySlacknessTheorem

29.3 Duality

The represented layer proves weak duality, extracts a dual certificate from a terminal SIMPLEX dictionary, derives strong duality, and proves both directions of complementary slackness.

Implementation details

The split proof layers remain available outside the main sidebar:

Dual Feasibility
Weak Duality
Optimality Specifications
Complementary-Slackness Gap Identity
Terminal Dual Certificate
Dictionary/Primal Bridge
Strong Duality
Complementary-Slackness Theorem

              namespace CLRSnamespace Chapter29end Chapter29end CLRS