Formalizing Polyhedra using Mathlib

This section formalizes the definitions from Chapter 2 of "Gröbner Bases and Convex Polytopes" by leveraging the existing cone and halfspace theories in Mathlib.

structure PolyhedralGeometry.Polyhedron (m : Type u_4) (ι : Type u_5) : Type (max u_4 u_5)

A Polyhedron is defined by the data of its H-representation (A, b).

• m_fin : Fintype m
• ι_fin : Fintype ι
• A : Matrix m ι ℝ
• b : m → ℝ
• toSet : Set (ι → ℝ)

  The set of points in ℝⁿ satisfying the inequalities A • x ≤ b.

theorem PolyhedralGeometry.Polyhedron.ext {m : Type u_4} {ι : Type u_5} {x y : Polyhedron m ι} (m_fin : x.m_fin = y.m_fin) (ι_fin : x.ι_fin = y.ι_fin) (A : x.A = y.A) (b : x.b = y.b) (toSet : x.toSet = y.toSet) : x = y

theorem PolyhedralGeometry.Polyhedron.ext_iff {m : Type u_4} {ι : Type u_5} {x y : Polyhedron m ι} : x = y ↔ x.m_fin = y.m_fin ∧ x.ι_fin = y.ι_fin ∧ x.A = y.A ∧ x.b = y.b ∧ x.toSet = y.toSet

theorem PolyhedralGeometry.mem_polyhedron_iff {ι : Type u_1} {m : Type u_2} [Fintype ι] [Fintype m] (P : Polyhedron m ι) : P.toSet = {x : ι → ℝ | P.A.mulVec x ≤ P.b}

theorem PolyhedralGeometry.Polyhedron.convex {ι : Type u_1} {m : Type u_2} [Fintype ι] [Fintype m] (P : Polyhedron m ι) : Convex ℝ P.toSet

A Polyhedron is a convex set.

theorem PolyhedralGeometry.Polyhedron.toSet_convex {ι : Type u_1} {m : Type u_2} [Fintype ι] [Fintype m] (P : Polyhedron m ι) : Convex ℝ P.toSet

structure PolyhedralGeometry.PolyhedralCone (m : Type u_4) (ι : Type u_5) extends PolyhedralGeometry.Polyhedron m ι : Type (max u_4 u_5)

A Polyhedral Cone is a special case of a polyhedron where b = 0.

• m_fin : Fintype m
• ι_fin : Fintype ι
• A : Matrix m ι ℝ
• b : m → ℝ
• toSet : Set (ι → ℝ)

theorem PolyhedralGeometry.PolyhedralCone.ext_iff {m : Type u_4} {ι : Type u_5} {x y : PolyhedralCone m ι} : x = y ↔ x.m_fin = y.m_fin ∧ x.ι_fin = y.ι_fin ∧ x.A = y.A ∧ x.b = y.b ∧ x.toSet = y.toSet

theorem PolyhedralGeometry.PolyhedralCone.ext {m : Type u_4} {ι : Type u_5} {x y : PolyhedralCone m ι} (m_fin : x.m_fin = y.m_fin) (ι_fin : x.ι_fin = y.ι_fin) (A : x.A = y.A) (b : x.b = y.b) (toSet : x.toSet = y.toSet) : x = y

structure PolyhedralGeometry.Polytope (ι : Type u_4) : Type u_4

The set of points in ℝⁿ satisfying the inequalities A • x ≤ 0.

• vertices : Finset (ι → ℝ)
• toSet : Set (ι → ℝ)

theorem PolyhedralGeometry.Polytope.ext_iff {ι : Type u_4} {x y : Polytope ι} : x = y ↔ x.vertices = y.vertices ∧ x.toSet = y.toSet

theorem PolyhedralGeometry.Polytope.ext {ι : Type u_4} {x y : Polytope ι} (vertices : x.vertices = y.vertices) (toSet : x.toSet = y.toSet) : x = y

theorem PolyhedralGeometry.Polytope.toSet_convex {ι : Type u_1} [Fintype ι] (P : Polytope ι) : Convex ℝ P.toSet

Section: Faces and Minkowski Addition (Adapted for new structures)

def PolyhedralGeometry.face {ι : Type u_1} [Fintype ι] (ω : ι → ℝ) (P : Set (ι → ℝ)) : Set (ι → ℝ)

Sturmfels, Chapter 2: faceω(P) := {u ∈ P : ω • u ≥ ω • v for all v ∈ P}

The face of a Polyhedron P. The input is a Polyhedron structure, not just a Set.

Equations

• PolyhedralGeometry.face ω P = {u : ι → ℝ | u ∈ P ∧ ∀ v ∈ P, ω ⬝ᵥ v ≤ ω ⬝ᵥ u}

def PolyhedralGeometry.IsFace {ι : Type u_1} {m : Type u_2} [Fintype ι] (F : Set (ι → ℝ)) (P : Polyhedron m ι) : Prop

Sturmfels, Chapter 2: "a face of P"

A subset F is a face of a Polyhedron P.

Equations

• PolyhedralGeometry.IsFace F P = (F ⊆ P.toSet ∧ ∃ (ω : ι → ℝ), F = PolyhedralGeometry.face ω P.toSet)

theorem PolyhedralGeometry.face_of_face_is_face {m : Type u_4} {ι : Type u_5} [Fintype m] [Fintype ι] (ω ω' : ι → ℝ) (P : Polyhedron m ι) : ∃ ε₀ > 0, ∀ (ε : ℕ), 0 < ε ∧ ε < ε₀ → face ω' (face ω P.toSet) = face (ω + ε • ω') P.toSet

Sturmfels, Chapter 2: faceω'(faceω(P)) = face(ω+ε·ω')(P)

structure Polyhedron (m : Type u_4) (ι : Type u_5) [Fintype m] [Fintype ι] : Type (max u_4 u_5)

A Polyhedron (H-representation) is a finite intersection of closed half-spaces. This definition directly translates the text: P = {x ∈ ℝⁿ : A • x ≤ b}.

Each row i of the matrix A and the corresponding entry b i defines a closed half-space {x | (A i) • x ≤ b i}. The polyhedron is the intersection of these.

• A : Matrix m ι ℝ
• b : m → ℝ
• toSet : Set (ι → ℝ)

  The set of points in ℝⁿ satisfying the inequalities A • x ≤ b.

theorem Polyhedron.ext_iff {m : Type u_4} {ι : Type u_5} {inst✝ : Fintype m} {inst✝¹ : Fintype ι} {x y : Polyhedron m ι} : x = y ↔ x.A = y.A ∧ x.b = y.b ∧ x.toSet = y.toSet

theorem Polyhedron.ext {m : Type u_4} {ι : Type u_5} {inst✝ : Fintype m} {inst✝¹ : Fintype ι} {x y : Polyhedron m ι} (A : x.A = y.A) (b : x.b = y.b) (toSet : x.toSet = y.toSet) : x = y

structure PolyhedralCone (m : Type u_4) (ι : Type u_5) [Fintype m] [Fintype ι] : Type (max u_4 u_5)

A Polyhedral Cone is a finite intersection of closed linear half-spaces. It is a special case of a polyhedron where b = 0. P = {x ∈ ℝⁿ : A • x ≤ 0}.

• A : Matrix m ι ℝ
• toSet : Set (ι → ℝ)

  The set of points in ℝⁿ satisfying the inequalities A • x ≤ 0.

theorem PolyhedralCone.ext_iff {m : Type u_4} {ι : Type u_5} {inst✝ : Fintype m} {inst✝¹ : Fintype ι} {x y : PolyhedralCone m ι} : x = y ↔ x.A = y.A ∧ x.toSet = y.toSet

theorem PolyhedralCone.ext {m : Type u_4} {ι : Type u_5} {inst✝ : Fintype m} {inst✝¹ : Fintype ι} {x y : PolyhedralCone m ι} (A : x.A = y.A) (toSet : x.toSet = y.toSet) : x = y

structure PolyhedralCone₂ (m : Type u_4) (ι : Type u_5) [Fintype m] [Fintype ι] : Type (max u_4 u_5)

• toPolyhedron : Polyhedron m ι

  The underlying polyhedron.

• b_is_zero : self.toPolyhedron.b = 0

  The proof that the vector b is zero.

theorem PolyhedralCone₂.ext_iff {m : Type u_4} {ι : Type u_5} {inst✝ : Fintype m} {inst✝¹ : Fintype ι} {x y : PolyhedralCone₂ m ι} : x = y ↔ x.toPolyhedron = y.toPolyhedron

theorem PolyhedralCone₂.ext {m : Type u_4} {ι : Type u_5} {inst✝ : Fintype m} {inst✝¹ : Fintype ι} {x y : PolyhedralCone₂ m ι} (toPolyhedron : x.toPolyhedron = y.toPolyhedron) : x = y