Carathéodory's convexity theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Convex hull can be regarded as a refinement of affine span. Both are closure operators but whereas convex hull takes values in the lattice of convex subsets, affine span takes values in the much coarser sublattice of affine subspaces.

The cost of this refinement is that one no longer has bases. However Carathéodory's convexity theorem offers some compensation. Given a set s together with a point x in its convex hull, Carathéodory says that one may find an affine-independent family of elements s whose convex hull contains x. Thus the difference from the case of affine span is that the affine-independent family depends on x.

In particular, in finite dimensions Carathéodory's theorem implies that 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

source

theorem caratheodory.mem_convex_hull_erase {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [decidable_eq E] {t : finset E} (h : ¬affine_independent 𝕜 coe) {x : E} (m : x ∈ ⇑(convex_hull 𝕜) ↑t) :

∃ (y : ↥↑t), x ∈ ⇑(convex_hull 𝕜) ↑(t.erase ↑y)

If x is in the convex hull of some finset t whose elements are not affine-independent, then it is in the convex hull of a strict subset of t.

source

noncomputable def caratheodory.min_card_finset_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) :

finset E

Given a point x in the convex hull of a set s, this is a finite subset of s of minimum cardinality, whose convex hull contains x.

Equations

caratheodory.min_card_finset_of_mem_convex_hull hx = function.argmin_on finset.card nat.lt_wf {t : finset E | ↑t ⊆ s ∧ x ∈ ⇑(convex_hull 𝕜) ↑t} _

source

theorem caratheodory.min_card_finset_of_mem_convex_hull_subseteq {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) :

↑(caratheodory.min_card_finset_of_mem_convex_hull hx) ⊆ s

source

theorem caratheodory.mem_min_card_finset_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) :

x ∈ ⇑(convex_hull 𝕜) ↑(caratheodory.min_card_finset_of_mem_convex_hull hx)

source

theorem caratheodory.min_card_finset_of_mem_convex_hull_nonempty {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) :

(caratheodory.min_card_finset_of_mem_convex_hull hx).nonempty

source

theorem caratheodory.min_card_finset_of_mem_convex_hull_card_le_card {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) {t : finset E} (ht₁ : ↑t ⊆ s) (ht₂ : x ∈ ⇑(convex_hull 𝕜) ↑t) :

(caratheodory.min_card_finset_of_mem_convex_hull hx).card ≤ t.card

source

theorem caratheodory.affine_independent_min_card_finset_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) :

affine_independent 𝕜 coe

source

theorem convex_hull_eq_union {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} :

⇑(convex_hull 𝕜) s = ⋃ (t : finset E) (hss : ↑t ⊆ s) (hai : affine_independent 𝕜 coe), ⇑(convex_hull 𝕜) ↑t

Carathéodory's convexity theorem

source

theorem eq_pos_convex_span_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull 𝕜) s) :

∃ (ι : Type u) (_x : fintype ι) (z : ι → E) (w : ι → 𝕜) (hss : set.range z ⊆ s) (hai : affine_independent 𝕜 z) (hw : ∀ (i : ι), 0 < w i), finset.univ.sum (λ (i : ι), w i) = 1 ∧ finset.univ.sum (λ (i : ι), w i • z i) = x

A more explicit version of convex_hull_eq_union.