Convex polyhedra

A convex polyhedron in a real topological vector space is the solution set of finitely many non-strict affine inequalities g i x ≤ 0, the g i being continuous affine functionals. This file introduces that predicate and the three closure properties a piecewise-linear calculus needs: a convex polyhedron is closed and convex, a finite intersection of convex polyhedra is one, and the preimage of one under a continuous affine map is one.

Those last two are exactly what makes the cells of a piecewise-affine decomposition composable: composing two piecewise-affine maps refines the source decomposition by pulling the target cells back along the affine pieces, and both operations must stay inside the class of cells.

The name is deliberately not IsPolyhedron. In piecewise-linear topology a polyhedron is a much weaker notion — a subset that is locally a cone, so a locally finite union of simplices, which need not be convex. The convex sets defined here are the cells out of which such a polyhedron is assembled.

Main definitions

• TauCeti.IsConvexPolyhedron: the solution set of finitely many non-strict affine inequalities.

Main results

• TauCeti.isConvexPolyhedron_setOf_forall: the defining form, with the inequalities indexed by an arbitrary finite type rather than by Fin n.
• TauCeti.IsConvexPolyhedron.isClosed and TauCeti.IsConvexPolyhedron.convex: a convex polyhedron is closed and convex, which is what its name claims.
• TauCeti.IsConvexPolyhedron.inter: an intersection of two convex polyhedra is one.
• TauCeti.IsConvexPolyhedron.preimage: the preimage of a convex polyhedron under a continuous affine map is one.

def TauCeti.IsConvexPolyhedron {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (s : Set E) : Prop

A convex polyhedron is the solution set of finitely many non-strict affine inequalities, the inequalities being given by continuous affine functionals.

Equations

• TauCeti.IsConvexPolyhedron s = ∃ (n : ℕ) (g : Fin n → E →ᴬ[ℝ] ℝ), s = {x : E | ∀ (i : Fin n), (g i) x ≤ 0}

theorem TauCeti.isConvexPolyhedron_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set E} : IsConvexPolyhedron s ↔ ∃ (n : ℕ) (g : Fin n → E →ᴬ[ℝ] ℝ), s = {x : E | ∀ (i : Fin n), (g i) x ≤ 0}

The finite affine inequalities characterizing a convex polyhedron.

theorem TauCeti.isConvexPolyhedron_setOf_forall {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_3} [Finite ι] (g : ι → E →ᴬ[ℝ] ℝ) : IsConvexPolyhedron {x : E | ∀ (i : ι), (g i) x ≤ 0}

The solution set of a finite family of non-strict affine inequalities, indexed by an arbitrary finite type, is a convex polyhedron. This is the form in which the definition is used: the constructions below produce their inequalities indexed by sums and products of index types.

theorem TauCeti.isConvexPolyhedron_setOf_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (g : E →ᴬ[ℝ] ℝ) : IsConvexPolyhedron {x : E | g x ≤ 0}

A single non-strict affine inequality cuts out a convex polyhedron.

theorem TauCeti.isConvexPolyhedron_univ {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] : IsConvexPolyhedron Set.univ

The whole space is a convex polyhedron: it is cut out by the empty family of inequalities.

theorem TauCeti.IsConvexPolyhedron.isClosed {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set E} (h : IsConvexPolyhedron s) : IsClosed s

A convex polyhedron is closed, being an intersection of preimages of Set.Iic 0 under continuous maps.

theorem TauCeti.IsConvexPolyhedron.convex {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set E} (h : IsConvexPolyhedron s) : Convex ℝ s

A convex polyhedron is convex: each defining inequality is preserved by affine combinations because the functional cutting it out is affine.

theorem TauCeti.IsConvexPolyhedron.inter {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s t : Set E} (hs : IsConvexPolyhedron s) (ht : IsConvexPolyhedron t) : IsConvexPolyhedron (s ∩ t)

An intersection of two convex polyhedra is a convex polyhedron: concatenate the two families of defining inequalities.

theorem TauCeti.IsConvexPolyhedron.preimage {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {u : Set F} (hu : IsConvexPolyhedron u) (A : E →ᴬ[ℝ] F) : IsConvexPolyhedron (⇑A ⁻¹' u)

The preimage of a convex polyhedron under a continuous affine map is a convex polyhedron: precompose each defining inequality with the map.