Finite exposed-face API for rational polytopes

Every nonempty exposed face of a finitely generated polytope is the convex hull of the generators which it contains. Consequently the custom face type used by this project is finite, even though an exposure is stored using arbitrary real affine data.

noncomputable def EGZ.RationalPolytope.Face.generatorFinset {n : ℕ} {P : RationalPolytope n} (F : P.Face) : Finset (RealCoord n)

The generators of P which lie on a face. This finite set uniquely determines the face.

Equations

• F.generatorFinset = {q ∈ P.generators | q ∈ F.carrier}

theorem EGZ.RationalPolytope.Face.generatorFinset_subset {n : ℕ} {P : RationalPolytope n} (F : P.Face) : F.generatorFinset ⊆ P.generators

theorem EGZ.RationalPolytope.Face.carrier_eq_convexHull_generatorFinset {n : ℕ} {P : RationalPolytope n} (F : P.Face) : F.carrier = (convexHull ℝ) ↑F.generatorFinset

An exposed face is the convex hull of precisely the chosen generators which lie on it.

theorem EGZ.RationalPolytope.Face.generatorFinset_nonempty {n : ℕ} {P : RationalPolytope n} (F : P.Face) : F.generatorFinset.Nonempty

Every nonempty exposed face contains at least one generator of the ambient polytope.

theorem EGZ.RationalPolytope.Face.generatorFinset_injective {n : ℕ} {P : RationalPolytope n} : Function.Injective generatorFinset

noncomputable def EGZ.RationalPolytope.Face.generatorCode {n : ℕ} {P : RationalPolytope n} (F : P.Face) : ↥P.generators.powerset

A code for a face as a member of the powerset of the given generating finset.

Equations

• F.generatorCode = ⟨F.generatorFinset, ⋯⟩

theorem EGZ.RationalPolytope.Face.generatorCode_injective {n : ℕ} {P : RationalPolytope n} : Function.Injective generatorCode

@[instance_reducible]

noncomputable instance EGZ.RationalPolytope.Face.faceFintype {n : ℕ} (P : RationalPolytope n) : Fintype P.Face

Equations

• EGZ.RationalPolytope.Face.faceFintype P = Fintype.ofInjective EGZ.RationalPolytope.Face.generatorCode ⋯

theorem EGZ.RationalPolytope.Face.convex {n : ℕ} {P : RationalPolytope n} (F : P.Face) : Convex ℝ F.carrier

A face carrier is convex.

@[instance_reducible]

noncomputable instance EGZ.RationalPolytope.Face.facePartialOrder {n : ℕ} (P : RationalPolytope n) : PartialOrder P.Face

Equations

• EGZ.RationalPolytope.Face.facePartialOrder P = PartialOrder.lift (fun (F : P.Face) => F.carrier) ⋯

@[simp]

theorem EGZ.RationalPolytope.Face.le_iff_carrier_subset {n : ℕ} {P : RationalPolytope n} {F G : P.Face} : F ≤ G ↔ F.carrier ⊆ G.carrier

def EGZ.RationalPolytope.Face.top {n : ℕ} (P : RationalPolytope n) : P.Face

The whole polytope is its top exposed face.

Equations

• EGZ.RationalPolytope.Face.top P = { carrier := P.carrier, is_exposed := ⋯, nonempty := ⋯ }

@[simp]

theorem EGZ.RationalPolytope.Face.top_carrier {n : ℕ} (P : RationalPolytope n) : (top P).carrier = P.carrier

@[instance_reducible]

noncomputable instance EGZ.RationalPolytope.Face.faceOrderTop {n : ℕ} (P : RationalPolytope n) : OrderTop P.Face

Equations

• EGZ.RationalPolytope.Face.faceOrderTop P = { top := EGZ.RationalPolytope.Face.top P, le_top := ⋯ }

def EGZ.RationalPolytope.Face.interOfNonempty {n : ℕ} {P : RationalPolytope n} (F G : P.Face) (hnonempty : (F.carrier ∩ G.carrier).Nonempty) : P.Face

The intersection of two faces is a face whenever it is nonempty.

Equations

• F.interOfNonempty G hnonempty = { carrier := F.carrier ∩ G.carrier, is_exposed := ⋯, nonempty := hnonempty }

@[simp]

theorem EGZ.RationalPolytope.Face.interOfNonempty_carrier {n : ℕ} {P : RationalPolytope n} (F G : P.Face) (hnonempty : (F.carrier ∩ G.carrier).Nonempty) : (F.interOfNonempty G hnonempty).carrier = F.carrier ∩ G.carrier

noncomputable def EGZ.RationalPolytope.Face.commonUpperMinCard {n : ℕ} {P : RationalPolytope n} (F G : P.Face) : ℕ

The least number of generators among common upper faces.

Equations

• F.commonUpperMinCard G = Nat.find ⋯

noncomputable def EGZ.RationalPolytope.Face.supFace {n : ℕ} {P : RationalPolytope n} (F G : P.Face) : P.Face

The common upper face with the fewest generating points. Intersecting with any other common upper face proves that it is the least one.

Equations

• F.supFace G = Classical.choose ⋯

theorem EGZ.RationalPolytope.Face.supFace_isLUB {n : ℕ} {P : RationalPolytope n} (F G : P.Face) : IsLUB {F, G} (F.supFace G)

@[instance_reducible]

noncomputable instance EGZ.RationalPolytope.Face.faceSemilatticeSup {n : ℕ} (P : RationalPolytope n) : SemilatticeSup P.Face

Equations

• EGZ.RationalPolytope.Face.faceSemilatticeSup P = SemilatticeSup.ofIsLUB EGZ.RationalPolytope.Face.supFace ⋯