A vertex's tight inequalities form an outer with a unique vertex
ProvedHirsch.target_tight_outer_unique_vertex_zero_diameterformalizationgraph-diameterpolyhedra
Let P={x in R^d : <a_i,x> <= b_i} be any finite H-polyhedron and let v be a vertex of P. There is a subpresentation consisting exactly of the inequalities tight at v. In that relaxed outer, v is the only vertex, and therefore the padded vertex-edge graph diameter is zero. The relaxed outer is allowed to be unbounded and may contain infinitely many nonvertex points. No boundedness, irredundancy, or full-dimensionality assumption is made.
Preamble
import Mathlib import Definitions.Def_Hirsch_model open scoped RealInnerProductSpace open Set
Formal statement
namespace Hirsch
theorem target_tight_outer_unique_vertex_zero_diameter
{d n : ℕ}
(a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
(v : EuclideanSpace ℝ (Fin d))
(hv : v ∈ Set.extremePoints ℝ (Hirsch.Hpoly a b)) :
∃ m : ℕ, m ≤ n ∧ ∃ e : Fin m ↪ Fin n,
(∀ i, (∃ k, e k = i) ↔ ⟪a i, v⟫ = b i) ∧
Set.extremePoints ℝ (Hirsch.Hpoly (fun k => a (e k)) (fun k => b (e k))) = {v} ∧
Hirsch.DiamLE (Hirsch.Hpoly (fun k => a (e k)) (fun k => b (e k))) 0 := by sorry
end HirschSource