Geometric rank bounds for repeated large faces

For a fixed nonempty set of points, faces which are least among the faces containing that set have strictly decreasing dimension in a nested polytope sequence satisfying the no-repetition condition.

theorem EGZ.RationalPolytope.Face.mem_of_mem_affineSpan {d : ℕ} {P : RationalPolytope d} (Γ : P.Face) {q : RealCoord d} (hqP : q ∈ P.carrier) (hq : q ∈ affineSpan ℝ Γ.carrier) : q ∈ Γ.carrier

An exposed face contains every polytope point in the affine span of its carrier.

theorem EGZ.RationalPolytope.Face.mem_of_mem_affineSpan_subset {d : ℕ} {P : RationalPolytope d} (Γ : P.Face) {S : Set (RealCoord d)} (hS : S ⊆ Γ.carrier) {q : RealCoord d} (hqP : q ∈ P.carrier) (hq : q ∈ affineSpan ℝ S) : q ∈ Γ.carrier

noncomputable def EGZ.RationalPolytope.Face.dimension {d : ℕ} {P : RationalPolytope d} (Γ : P.Face) : ℕ

Dimension of the affine hull of a face.

Equations

• Γ.dimension = Module.finrank ℝ ↥(affineSpan ℝ Γ.carrier).direction

theorem EGZ.RationalPolytope.Face.dimension_le {d : ℕ} {P : RationalPolytope d} (Γ : P.Face) : Γ.dimension ≤ d

theorem EGZ.RationalPolytope.Face.dimension_lt_of_subset_of_witness {d : ℕ} {P Q : RationalPolytope d} (Γ : P.Face) (Δ : Q.Face) (hsub : Γ.carrier ⊆ Δ.carrier) (hw : ∃ q ∈ Δ.carrier, q ∈ P.carrier ∧ q ∉ Γ.carrier) : Γ.dimension < Δ.dimension

If an upper carrier contains a face and a point of the same polytope outside it, its affine dimension is strictly greater.

def EGZ.RationalPolytope.Face.MinimallyContains {d : ℕ} {P : RationalPolytope d} (Γ : P.Face) (S : Set (RealCoord d)) : Prop

A face is the least face containing a prescribed set.

Equations

• Γ.MinimallyContains S = (S ⊆ Γ.carrier ∧ ∀ (Δ : P.Face), S ⊆ Δ.carrier → Γ.carrier ⊆ Δ.carrier)

theorem EGZ.RationalPolytope.Face.exists_proper_subface_of_not_minimallyContains {d : ℕ} {P : RationalPolytope d} (Γ : P.Face) {S : Set (RealCoord d)} (hSne : S.Nonempty) (hS : S ⊆ Γ.carrier) (hnot : ¬Γ.MinimallyContains S) : ∃ (Δ : P.Face), S ⊆ Δ.carrier ∧ Δ.carrier ⊂ Γ.carrier

Failure of leastness supplies a proper subface still containing the set.

theorem EGZ.RationalPolytope.Face.dimension_lt_of_nested_minimallyContains {d : ℕ} {P Q : RationalPolytope d} (Γ : P.Face) (Δ : Q.Face) (hQP : Q.carrier ⊆ P.carrier) {S : Set (RealCoord d)} (hSne : S.Nonempty) (hSΓ : S ⊆ Γ.carrier) (hΔ : Δ.MinimallyContains S) (hne : Γ.carrier ∩ Q.carrier ≠ Δ.carrier) : Δ.dimension < Γ.dimension

Least containing faces have strictly decreasing dimensions across two nested polytopes when the old face does not restrict to the new one.

theorem EGZ.RationalPolytope.Face.card_minimallyContains_le {d N : ℕ} (P : Fin N → RationalPolytope d) (Γ : (i : Fin N) → (P i).Face) (hnested : ∀ (i j : Fin N), i < j → (P j).carrier ⊆ (P i).carrier) (hdistinct : ∀ (i j : Fin N), i < j → (Γ i).carrier ∩ (P j).carrier ≠ (Γ j).carrier) {S : Set (RealCoord d)} (hS : S.Nonempty) : {i : Fin N | (Γ i).MinimallyContains S}.card ≤ d + 1

At most d+1 members of a nested no-repetition sequence can be least containing faces for a fixed nonempty set.