Finite convex hulls in convex position

This file bridges the operational notion of convex position used in the proof of Theorem 1.12 with mathlib's ConvexIndependent, and constructs the rational polytope whose vertices are exactly a given rational family in convex position.

def EGZ.IsInConvexPosition {d n : ℕ} (points : Fin n → RealCoord d) : Prop

The paper's finite-family notion of convex position, in the operational form needed by Definition 3.7.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.IsInConvexPosition.convexIndependent {d n : ℕ} {points : Fin n → RealCoord d} (hpos : IsInConvexPosition points) (hinjective : Function.Injective points) : ConvexIndependent ℝ points

For an injective family, the operational definition of convex position implies mathlib's set-theoretic convex independence.

theorem EGZ.IsInConvexPosition.extremePoints_convexHull_range {d n : ℕ} {points : Fin n → RealCoord d} (hpos : IsInConvexPosition points) (hinjective : Function.Injective points) : Set.extremePoints ℝ ((convexHull ℝ) (Set.range points)) = Set.range points

An injective family in operational convex position is exactly the vertex set of its convex hull.

theorem EGZ.exists_openSegment_of_mem_intrinsicInterior {d : ℕ} {C : Set (RealCoord d)} {q x : RealCoord d} (hq : q ∈ intrinsicInterior ℝ C) (hx : x ∈ C) (hqx : q ≠ x) : ∃ z ∈ C, q ∈ openSegment ℝ x z

A relative-interior point can be extended past any distinct point of the set. Equivalently, it is a strict convex combination of that point and a second point of the set. This elementary form is particularly convenient when positive coefficients on a prescribed finite support must be retained.

structure EGZ.FiniteHullModel {d n : ℕ} (points : Fin n → RealCoord d) : Type

A finite convex hull together with the vertex identification needed in the hollow-polytope branch.

• polytope : RationalPolytope d

  Rational polytope realizing the finite hull.

• carrier_eq : self.polytope.carrier = (convexHull ℝ) (Set.range points)
• vertexSet_eq : self.polytope.vertexSet = Set.range points

noncomputable def EGZ.finiteHullModel {d n : ℕ} (points : Fin n → RealCoord d) (hn : 0 < n) (hinjective : Function.Injective points) (hrational : ∀ (i : Fin n), IsRational (points i)) (hpos : IsInConvexPosition points) : FiniteHullModel points

The finite hull of a nonempty rational family in convex position, with its vertex set identified exactly.

Equations

• EGZ.finiteHullModel points hn hinjective hrational hpos = { polytope := EGZ.RationalPolytope.ofFiniteConvexHull (Set.range points) ⋯ ⋯ ⋯, carrier_eq := ⋯, vertexSet_eq := ⋯ }