Finite convex combinations of polytope vertices

This file packages membership in the convex hull of the vertex set as a finite family of real weights. Real weights are necessary for an arbitrary real point of a rational polytope: even an interval with rational endpoints contains points which admit no rational convex coefficients.

The support lemmas record the two properties needed by reductions to finite vertex families. A positive summand of a combination lying on an exposed face lies on that face, and a positive summand of a combination equal to a vertex must be that vertex.

noncomputable def EGZ.RationalPolytope.vertexFinset {d : ℕ} (P : RationalPolytope d) : Finset (RealCoord d)

The finite set of actual vertices of a rational polytope.

Equations

• P.vertexFinset = ⋯.toFinset

@[simp]

theorem EGZ.RationalPolytope.coe_vertexFinset {d : ℕ} (P : RationalPolytope d) : ↑P.vertexFinset = P.vertexSet

@[simp]

theorem EGZ.RationalPolytope.mem_vertexFinset {d : ℕ} (P : RationalPolytope d) {v : RealCoord d} : v ∈ P.vertexFinset ↔ v ∈ P.vertexSet

theorem EGZ.RationalPolytope.vertexFinset_subset_carrier {d : ℕ} (P : RationalPolytope d) {v : RealCoord d} : v ∈ P.vertexFinset → v ∈ P.carrier

structure EGZ.RationalPolytope.VertexWeights {d : ℕ} (P : RationalPolytope d) (q : RealCoord d) : Type

A convex combination indexed by the complete finite vertex set of P.

The weight is stored on the ambient coordinate type because this is the form returned by Finset.mem_convexHull' and is convenient when a later argument supplies coefficients vertex by vertex. Only its values on vertexFinset enter the data.

• weight : RealCoord d → ℝ

  Barycentric weight assigned to each vertex.

• nonnegative (v : RealCoord d) : v ∈ P.vertexFinset → 0 ≤ self.weight v
• sum_eq_one : ∑ v ∈ P.vertexFinset, self.weight v = 1
• weighted_sum_eq : ∑ v ∈ P.vertexFinset, self.weight v • v = q

theorem EGZ.RationalPolytope.exists_vertexWeights {d : ℕ} (P : RationalPolytope d) {q : RealCoord d} (hq : q ∈ P.carrier) : Nonempty (P.VertexWeights q)

Every point of a rational polytope has a finite convex-combination representation using all of its vertices (with zero weights permitted).

theorem EGZ.RationalPolytope.eq_of_pos_of_eq_convexCombination_of_mem_vertexSet {d : ℕ} {P : RationalPolytope d} {I : Type u_1} [Fintype I] (points : I → RealCoord d) (weight : I → ℝ) (q : RealCoord d) (hpoints : ∀ (i : I), points i ∈ P.carrier) (hweight0 : ∀ (i : I), 0 ≤ weight i) (hweightsum : ∑ i : I, weight i = 1) (hbary : q = ∑ i : I, weight i • points i) (hq : q ∈ P.vertexSet) {i : I} (hi : 0 < weight i) : points i = q

In any finite convex combination equal to an extreme point of P, a strictly positive summand is that extreme point. The inputs need only lie in P; they need not themselves be vertices.

This indexed form is convenient for zero-sum reductions, whose coefficients are naturally indexed by the original finite family.

theorem EGZ.RationalPolytope.VertexWeights.mem_face_of_pos {d : ℕ} {P : RationalPolytope d} {q : RealCoord d} (W : P.VertexWeights q) (F : P.Face) (hqF : q ∈ F.carrier) {v : RealCoord d} (hv : v ∈ P.vertexFinset) (hpos : 0 < W.weight v) : v ∈ F.carrier

If the represented point lies in an exposed face, every vertex carrying positive weight lies in that face.

theorem EGZ.RationalPolytope.VertexWeights.eq_of_pos_of_mem_vertexSet {d : ℕ} {P : RationalPolytope d} {q : RealCoord d} (W : P.VertexWeights q) (hq : q ∈ P.vertexSet) {v : RealCoord d} (hv : v ∈ P.vertexFinset) (hpos : 0 < W.weight v) : v = q

In a convex representation of an extreme point of P, every vertex with positive weight is the represented point itself.

theorem EGZ.RationalPolytope.VertexWeights.weight_eq_zero_of_mem_vertexSet_of_ne {d : ℕ} {P : RationalPolytope d} {q : RealCoord d} (W : P.VertexWeights q) (hq : q ∈ P.vertexSet) {v : RealCoord d} (hv : v ∈ P.vertexFinset) (hvq : v ≠ q) : W.weight v = 0

Equivalently, every vertex different from an extreme represented point has zero weight.