mathlibdocumentation

analysis.convex.caratheodory

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

theorem caratheodory.mem_convex_hull_erase {E : Type u} [ E] [decidable_eq E] {t : finset E} (h : < t.card) {x : E} :
(∃ (y : t), x convex_hull (t.erase y))

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.

theorem caratheodory.step {E : Type u} [ E] [decidable_eq E] (t : finset E) :
< t.card = ⋃ (x : t), convex_hull (t.erase x))

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.

theorem caratheodory.shrink' {E : Type u} [ E] (t : finset E) (k : ) :
t.card = + k ⋃ (t' : finset E) (w : t' t) (b : t'.card , convex_hull 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.

theorem caratheodory.shrink {E : Type u} [ E] (t : finset E) :
⋃ (t' : finset E) (w : t' t) (b : t'.card ,

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.

theorem convex_hull_subset_union {E : Type u} [ E] (s : set E) :
⋃ (t : finset E) (w : t s) (b : t.card ,

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.

theorem convex_hull_eq_union {E : Type u} [ E] (s : set E) :
= ⋃ (t : finset E) (w : t s) (b : t.card ,

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.

theorem eq_center_mass_card_le_dim_succ_of_mem_convex_hull {E : Type u} [ E] {s : set E} {x : E} :
x (∃ (t : finset E) (w : t s) (b : t.card (f : E → ), (∀ (y : E), y t0 f y) t.sum f = 1 t.center_mass f id = x)

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.

theorem eq_pos_center_mass_card_le_dim_succ_of_mem_convex_hull {E : Type u} [ E] {s : set E} {x : E} :
x (∃ (t : finset E) (w : t s) (b : t.card (f : E → ), (∀ (y : E), y t0 < f y) t.sum f = 1 t.center_mass f id = x)

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.)