mathlib documentation

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:

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.

theorem caratheodory.shrink' {E : Type u} [add_comm_group E] [vector_space E] [finite_dimensional E] (t : finset E) (k : ) :

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} [add_comm_group E] [vector_space E] [finite_dimensional E] (t : finset E) :
convex_hull t ⋃ (t' : finset E) (w : t' t) (b : t'.card finite_dimensional.findim E + 1), convex_hull t'

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.

theorem convex_hull_eq_union {E : Type u} [add_comm_group E] [vector_space E] [finite_dimensional E] (s : set E) :

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} [add_comm_group E] [vector_space E] [finite_dimensional E] {s : set E} {x : E} :
x convex_hull s(∃ (t : finset E) (w : t s) (b : t.card finite_dimensional.findim E + 1) (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} [add_comm_group E] [vector_space E] [finite_dimensional E] {s : set E} {x : E} :
x convex_hull s(∃ (t : finset E) (w : t s) (b : t.card finite_dimensional.findim E + 1) (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.)