|
Linear
Inequalities
Title: |
Linear Inequalities |
Authors:
|
Ralph Bottesch,
Alban Reynaud and
René Thiemann
|
Submission date: |
2019-06-21 |
Abstract: |
We formalize results about linear inqualities, mainly from
Schrijver's book. The main results are the proof of the
fundamental theorem on linear inequalities, Farkas' lemma,
Carathéodory's theorem, the Farkas-Minkowsky-Weyl theorem, the
decomposition theorem of polyhedra, and Meyer's result that the
integer hull of a polyhedron is a polyhedron itself. Several theorems
include bounds on the appearing numbers, and in particular we provide
an a-priori bound on mixed-integer solutions of linear inequalities. |
BibTeX: |
@article{Linear_Inequalities-AFP,
author = {Ralph Bottesch and Alban Reynaud and René Thiemann},
title = {Linear Inequalities},
journal = {Archive of Formal Proofs},
month = jun,
year = 2019,
note = {\url{http://isa-afp.org/entries/Linear_Inequalities.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
LLL_Basis_Reduction |
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.
|
|