Reservoir

Duality theory in linear optimization and its extensions

Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems in Lean 4. Furthermore, we consider a linearly ordered field extended with two special elements denoted by and where is below every element and is above every element. We define for all and we define for all . Instead of multiplication, we define scalar action for every but we define only for because . We extend certain Farkas-like theorems to a setting where coefficients are from an extended linearly ordered field.

Technical report

Main corollaries

• Farkas for equalities
• Farkas for inequalities
• Strong duality for standard LP

Main results

• Farkas-Bartl theorem
• Extended Farkas theorem
• Strong duality for extended LP