Linear programming: maximum principle and vertex optimality
lp_maximum_principle
Submitter: Kim Morrison.
Notes: §101 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' gives two structural facts for linear programs in standard inequality form: maximise c·x subject to A x ≤ b and 0 ≤ x. The maximum principle says any local maximiser of the linear objective on the feasible region is global, and if c ≠ 0 then it lies on the feasible region's frontier. The vertex optimality statement says that a nonempty bounded feasible region has an optimal solution at an extreme point (the existence content of Dantzig's simplex algorithm). Mathlib has the relevant convex-geometry notions, including IsLocalMaxOn, IsMaxOn, frontier, Set.extremePoints, and Krein–Milman-style infrastructure, but not these LP results as named theorems.
Source: G. B. Dantzig (1947), simplex algorithm. Listed as §101 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).
Informal solution: Maximum principle: the objective x ↦ c·x is affine, hence both concave and convex, and the feasible region {x | A x ≤ b, 0 ≤ x} is convex. A local maximum of a concave function on a convex set is global: for any feasible y, the segment x + t(y − x) stays feasible and the objective along it is affine, so if it does not exceed the value at x for small t it cannot at t = 1 either. For the frontier claim, if c ≠ 0 then c·x is a non-constant affine functional, which on a convex set cannot attain its maximum at an interior point (moving in the direction +c stays inside a small ball and strictly increases the objective), so the maximiser is on the frontier. Vertex optimality: a nonempty bounded feasible region of an LP is a compact convex polytope, so by Krein–Milman it is the closed convex hull of its extreme points and the continuous objective attains its maximum; among maximisers, an extreme point of the face on which the maximum is attained is an extreme point of the whole region, giving an optimal vertex.
/-- **Maximum principle for linear programming** (§101). A local maximiser of
the LP objective on the feasible region is automatically a global maximiser; and
whenever the objective is non-constant (`c ≠ 0`), the maximiser lies on the
topological frontier of the feasible region. -/
theorem declaration uses `sorry`lp_maximum_principle {m n : ℕ} (lp : LinearProgram m n)
(x : Fin m → ℝ) (_hx : x ∈ lp.feasible)
(_hlocal : IsLocalMaxOn lp.objective lp.feasible x) :
IsMaxOn lp.objective lp.feasible x ∧
(lp.c ≠ 0 → x ∈ frontier lp.feasible) := m:ℕn:ℕlp:LinearProgram m nx:Fin m → ℝ_hx:x ∈ lp.feasible_hlocal:IsLocalMaxOn lp.objective lp.feasible x⊢ IsMaxOn lp.objective lp.feasible x ∧ (lp.c ≠ 0 → x ∈ frontier lp.feasible)
All goals completed! 🐙/-- **Vertex optimality** (§101; the existence content of Dantzig's 1947 simplex
algorithm). Every linear program with a nonempty bounded feasible region admits a
global maximiser that is an extreme point (vertex) of the feasible region. -/
theorem declaration uses `sorry`simplex_algorithm {m n : ℕ} (lp : LinearProgram m n)
(_hfeas : lp.feasible.Nonempty) (_hbdd : Bornology.IsBounded lp.feasible) :
∃ x ∈ lp.feasible, IsMaxOn lp.objective lp.feasible x ∧
x ∈ Set.extremePoints ℝ lp.feasible := m:ℕn:ℕlp:LinearProgram m n_hfeas:lp.feasible.Nonempty_hbdd:Bornology.IsBounded lp.feasible⊢ ∃ x ∈ lp.feasible, IsMaxOn lp.objective lp.feasible x ∧ x ∈ Set.extremePoints ℝ lp.feasible
All goals completed! 🐙Solved by
• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 2, 2026
• @GanjinZero with Seed Prover (ByteDance) on Jun 3, 2026
• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026
• @rishistyping with Stealth Model on Jun 7, 2026