Polytopes, triangulation, and local simpliciality

Every polyhedral convex set is locally simplicial. This is the result that supplies instances of LocallySimplicial, and with them the continuity theorems that consume it.

Around a point x of a polyhedral set C, cut out a bounded polyhedral neighbourhood V; then V ∩ C is a bounded polyhedral convex set, hence a polytope — the direction part of conv P + cone D has to vanish — hence, by Carathéodory's theorem, a finite union of simplices, all of them inside C.

Main results

• exists_polyhedral_isBounded_mem_nhds — every point has a bounded polyhedral neighbourhood: a coordinate cube for a basis. This is the only place a basis is used.
• Polyhedral.exists_finset_convexHull — a bounded polyhedral convex set is the convex hull of a finite set.
• isSimplex_convexHull_coe — the convex hull of an affinely independent Finset is a simplex.
• Polyhedral.locallySimplicial — every polyhedral convex set is locally simplicial (Theorem 20.5 in [^1]).
• exists_polyhedral_between — a compact set inside int D is inside int P for some polyhedral P ⊆ int D.

Implementation notes

The classical proof takes V to be a simplex; here it is a cube, cheaper to build and all the argument needs — 2 n inequalities ± bᵢ* (y - x) ≤ 1 for a basis b, bounded because ‖y - x‖ ≤ ∑ ‖bᵢ‖ on it, and a neighbourhood because the strict version is open. The triangulation is Mathlib's convexHull_eq_union read as a finite union: for a finite generating set the index set is P.powerset, and Finset.equivFin turns it into the Fin n-indexed family LocallySimplicial asks for.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §20.

theorem Tdaf.ConvexAnalysis.exists_polyhedral_mem_nhds_subset_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) {ε : ℝ} (hε : 0 < ε) : ∃ (V : Set E), Polyhedral V ∧ Bornology.IsBounded V ∧ V ∈ nhds x ∧ V ⊆ Metric.ball x ε

Every point of a finite-dimensional space has arbitrarily small bounded polyhedral neighbourhoods: the coordinate cubes {y | ∀ i, |bᵢ* (y - x)| ≤ c} of a basis b.

theorem Tdaf.ConvexAnalysis.exists_polyhedral_isBounded_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : ∃ (V : Set E), Polyhedral V ∧ Bornology.IsBounded V ∧ V ∈ nhds x

Every point of a finite-dimensional space has a bounded polyhedral neighbourhood.

theorem Tdaf.ConvexAnalysis.Polyhedral.exists_finset_convexHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Polyhedral C) (hbdd : Bornology.IsBounded C) : ∃ (P : Finset E), C = (convexHull ℝ) ↑P

A bounded polyhedral convex set is a polytope: the convex hull of a finite set of points. Minkowski–Weyl writes it as conv P + cone D, and boundedness kills every generator of the cone.

theorem Tdaf.ConvexAnalysis.isSimplex_convexHull_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : Finset E} (ht : AffineIndependent ℝ Subtype.val) : IsSimplex ((convexHull ℝ) ↑t)

The convex hull of an affinely independent Finset is a simplex. The index type of IsSimplex is a Type (universe 0), so the subtype ↥t is transported to Fin t.card.

theorem Tdaf.ConvexAnalysis.Polyhedral.locallySimplicial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Polyhedral C) : LocallySimplicial C

Every polyhedral convex set is locally simplicial — and in particular every polytope is.

This is what makes the continuity results of Simplicial.lean usable: until now LocallySimplicial had no supply of instances beyond simplices themselves.

theorem Tdaf.ConvexAnalysis.exists_polyhedral_between {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C D : Set E} (hCcl : IsClosed C) (hCbdd : Bornology.IsBounded C) (hD : Convex ℝ D) (hCD : C ⊆ interior D) : ∃ (P : Set E), Polyhedral P ∧ P ⊆ interior D ∧ C ⊆ interior P

A compact set inside the interior of a convex set can be separated from the boundary by a polyhedral convex set: there is a polyhedral P with C ⊆ int P and P ⊆ int D.

The classical proof covers C by simplices; a cover by coordinate cubes does the same job and is what exists_polyhedral_mem_nhds_subset_ball already supplies. The polyhedral set is then the convex hull of the finitely many cubes' vertex sets, polyhedral because a convex hull of a finite set is.

Convexity of C is not used, and neither is nonemptiness — the classical statement assumes both, but the covering argument needs only that C is compact.