Duality theory in linear optimization and its extensions -- formally verified
Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally verified. arXiv, 2409.08119.
Download (ext.)
Preprint
| Submitted
| English
Corresponding author has ISTA affiliation
Department
Abstract
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 over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".
Publishing Year
Date Published
2024-09-12
Journal Title
arXiv
Acknowledgement
We would like to thank David Bartl and Jasmin Blanchette for frequent consultations. We would also like to express gratitude to Andrew Yang for the proof of Finset.univ sum of zero when not and to Henrik B¨oving for a help with generalization from extended rationals to extended linearly ordered fields. We would also like to acknowledge Antoine Chambert-Loir, Apurva Nakade, Ya¨el Dillies, Richard Copley, Edward van de Meent, Markus Himmel, Mario Carneiro, and Kevin Buzzard.
Article Number
2409.08119
IST-REx-ID
Cite this
Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally verified. arXiv. doi:10.48550/arXiv.2409.08119
Dvorak, M., & Kolmogorov, V. (n.d.). Duality theory in linear optimization and its extensions -- formally verified. arXiv. https://doi.org/10.48550/arXiv.2409.08119
Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally Verified.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2409.08119.
M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its extensions -- formally verified,” arXiv. .
Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally verified. arXiv, 2409.08119.
Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally Verified.” ArXiv, 2409.08119, doi:10.48550/arXiv.2409.08119.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Software:
Description
full version of all definitions, statement, and proofs
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 2409.08119
Google Scholar