The polytope centerpoint theorem

This module assembles the canonical support-hull face flag, Flag Helly and its centerpoint corollary, and the prime-reduction bound for hollow rational polytopes into Theorem 1.12.

theorem EGZ.theorem_1_12_polytope_centerpoint {d : ℕ} (hd : 0 < d) (P : RationalPolytope d) (w : RealCoord d → NNReal) (hfinite : (Function.support w).Finite) (hnonzero : w ≠ 0) (hsupport : Function.support w ⊆ P.carrier) (hrational : ∀ q ∈ Function.support w, IsRational q) : PolytopeCenterpointConclusion P w

Theorem 1.12 (thm:cpt), with the rational-support hypothesis made explicit. In the paper this is intended by P ⊆ ℚ^d; it is necessary once the polytope is represented in its real affine span.