Carathéodory's convexity theorem
This file is devoted to proving Carathéodory's convexity theorem:
The convex hull of a set s in ℝᵈ is the union of the convex hulls of the (d+1)-tuples in s.
Main results:
convex_hull_eq_union: Carathéodory's convexity theorem
Implementation details
This theorem was formalized as part of the Sphere Eversion project.
Tags
convex hull, caratheodory
If x is in the convex hull of some finset t with strictly more than findim + 1 elements,
then it is in the union of the convex hulls of the finsets t.erase y for y ∈ t.
The convex hull of a finset t with findim ℝ E + 1 < t.card is equal to
the union of the convex hulls of the finsets t.erase x for x ∈ t.
The convex hull of a finset t with findim ℝ E + 1 < t.card is contained in
the union of the convex hulls of the finsets t' ⊆ t with t'.card ≤ findim ℝ E + 1.
The convex hull of any finset t is contained in
the union of the convex hulls of the finsets t' ⊆ t with t'.card ≤ findim ℝ E + 1.
One inclusion of Carathéodory's convexity theorem.
The convex hull of a set s in ℝᵈ is contained in
the union of the convex hulls of the (d+1)-tuples in s.
Carathéodory's convexity theorem.
The convex hull of a set s in ℝᵈ is the union of the convex hulls of the (d+1)-tuples in s.
A more explicit formulation of Carathéodory's convexity theorem,
writing an element of a convex hull as the center of mass
of an explicit finset with cardinality at most dim + 1.
A variation on Carathéodory's convexity theorem,
writing an element of a convex hull as a center of mass
of an explicit finset with cardinality at most dim + 1,
where all coefficients in the center of mass formula
are strictly positive.
(This is proved using eq_center_mass_card_le_dim_succ_of_mem_convex_hull,
and discarding any elements of the set with coefficient zero.)