Why the selected flag centerpoint is interior #
On a finite support, a sufficiently large multiple of a face's exposing functional suppresses all points outside that face. This gives the halfspaces needed to show that the centerpoint's least face is large.
theorem
EGZ.RationalPolytope.Face.exists_halfspace_subset_sdiff
{r : ℕ}
{P : RationalPolytope r}
(F G : P.Face)
{c : RealCoord r}
(hcF : c ∈ F.carrier)
(hcG : c ∉ G.carrier)
(S : Finset (IntCoord r))
(hS : S.Nonempty)
(hSP : ∀ q ∈ S, q.real ∈ P.carrier)
:
A halfspace through a point of F \ G whose intersection with a
prescribed finite support lies in F \ G.
theorem
EGZ.FlagDecomposition.realized_face_eq_top_of_point
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(q : Φ.flag.Point)
(hq : q ∈ Φ.omega)
(F : (Φ.flag.polytope q.base).Face)
(hqF : q.val ∈ F.carrier)
(hreal : Φ.IsRealizedFace q.base F)
:
A proper point based at x cannot lie on a realized proper face at
x: its own base occurs in the supremum defining the face index.
theorem
EGZ.FlagDecomposition.centerpoint_mem_interior
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(hp : Odd p)
(q : Φ.flag.Point)
(hq : q ∈ Φ.omega)
{ε : ℝ}
(hε : 0 ≤ ε)
(hcentral :
∀ (ξ : RealCoord (Φ.flag.rank q.base) →ᵃ[ℝ] ℝ),
ε * ↑Φ.retainedMass ≤ ↑(Φ.liftedMassOn q.base {z : RealCoord (Φ.flag.rank q.base) | ξ q.val ≤ ξ z}))
(hfaces : ∀ (F : (Φ.flag.polytope q.base).Face), Φ.IsLargeFace ε q.base F → Φ.IsRealizedFace q.base F)
:
Completeness forces a proper centerpoint to lie in the relative interior of its base polytope. This includes rank zero.