Documentation

LeanPool.ErdosGinzburgZiv.EGZ.Convex.FaceCombinations

Convex combinations and minimal faces of rational polytopes #

This file develops the order-theoretic face API needed by the canonical face flag. Positivity in an exposed face forces every positive summand into that face. Relative-interior membership consequently implies that the face is the least face containing the point. Independently, finiteness of the face poset constructs such a least face for every point of the polytope.

source
theorem EGZ.RationalPolytope.Face.mem_of_pos_of_eq_convexCombination {d : ℕ} {P : RationalPolytope d} (F : P.Face) {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) (hqF : q ∈ F.carrier) {i : I} (hi : 0 < weight i) :
points i ∈ F.carrier

If a convex combination belongs to an exposed face, every input with strictly positive weight belongs to that face.

source
theorem EGZ.RationalPolytope.Face.le_of_mem_relInterior {d : ℕ} {P : RationalPolytope d} {F G : P.Face} {q : RealCoord d} (hqF : q ∈ F.relInterior) (hqG : q ∈ G.carrier) :
F ≤ G

A point in the relative interior of a face belongs to no smaller face: the relative-interior face lies below every face containing the point.

source
theorem EGZ.RationalPolytope.Face.eq_of_mem_relInterior {d : ℕ} {P : RationalPolytope d} {F G : P.Face} {q : RealCoord d} (hqF : q ∈ F.relInterior) (hqG : q ∈ G.relInterior) :
F = G

Relative interiors of distinct faces are disjoint.

source
def EGZ.RationalPolytope.Face.IsLeastFaceAt {d : ℕ} (P : RationalPolytope d) (q : RealCoord d) (F : P.Face) :
Prop

Order-theoretic minimality among the faces which contain a point.

Equations
Instances For
    source
    theorem EGZ.RationalPolytope.Face.exists_isLeastFaceAt {d : ℕ} (P : RationalPolytope d) {q : RealCoord d} (hq : q ∈ P.carrier) :
    ∃ (F : P.Face), IsLeastFaceAt P q F

    Every point of a rational polytope has a least containing face. This is purely finite: choose a containing face with the fewest generators, then intersect it with any competing containing face.

    source
    theorem EGZ.RationalPolytope.Face.isLeastFaceAt_of_mem_relInterior {d : ℕ} {P : RationalPolytope d} {q : RealCoord d} {F : P.Face} (hq : q ∈ F.relInterior) :
    IsLeastFaceAt P q F

    Relative-interior membership implies order-theoretic minimality.

    source
    theorem EGZ.RationalPolytope.Face.IsLeastFaceAt.unique {d : ℕ} {P : RationalPolytope d} {q : RealCoord d} {F G : P.Face} (hF : IsLeastFaceAt P q F) (hG : IsLeastFaceAt P q G) :
    F = G

    Order-theoretic least faces are unique.