mathlib documentation

analysis.convex.hull

Convex hull #

This file defines the convex hull of a set s in a module. convex_hull π•œ s is the smallest convex set containing s. In order theory speak, this is a closure operator.

Implementation notes #

convex_hull is defined as a closure operator. This gives access to the closure_operator API while the impact on writing code is minimal as convex_hull π•œ s is automatically elaborated as ⇑(convex_hull π•œ) s.

def convex_hull (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :

The convex hull of a set s is the minimal convex set that includes s.

Equations
theorem subset_convex_hull (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (s : set E) :
s βŠ† ⇑(convex_hull π•œ) s
theorem convex_convex_hull (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (s : set E) :
convex π•œ (⇑(convex_hull π•œ) s)
theorem convex_hull_min {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s t : set E} (hst : s βŠ† t) (ht : convex π•œ t) :
⇑(convex_hull π•œ) s βŠ† t
theorem convex_hull_mono {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s t : set E} (hst : s βŠ† t) :
⇑(convex_hull π•œ) s βŠ† ⇑(convex_hull π•œ) t
theorem convex.convex_hull_eq {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) :
⇑(convex_hull π•œ) s = s
@[simp]
theorem convex_hull_univ {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
@[simp]
theorem convex_hull_empty {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
@[simp]
theorem convex_hull_empty_iff {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} :
@[simp]
theorem convex_hull_nonempty_iff {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} :
@[simp]
theorem convex_hull_singleton {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {x : E} :
⇑(convex_hull π•œ) {x} = {x}
theorem convex.convex_remove_iff_not_mem_convex_hull_remove {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (x : E) :
convex π•œ (s \ {x}) ↔ x βˆ‰ ⇑(convex_hull π•œ) (s \ {x})
theorem is_linear_map.image_convex_hull {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set E} {f : E β†’ F} (hf : is_linear_map π•œ f) :
f '' ⇑(convex_hull π•œ) s = ⇑(convex_hull π•œ) (f '' s)
theorem linear_map.image_convex_hull {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set E} (f : E β†’β‚—[π•œ] F) :
⇑f '' ⇑(convex_hull π•œ) s = ⇑(convex_hull π•œ) (⇑f '' s)
theorem is_linear_map.convex_hull_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {f : E β†’ F} (hf : is_linear_map π•œ f) (s : set E) :
⇑(convex_hull π•œ) (f '' s) = f '' ⇑(convex_hull π•œ) s
theorem linear_map.convex_hull_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] (f : E β†’β‚—[π•œ] F) (s : set E) :
⇑(convex_hull π•œ) (⇑f '' s) = ⇑f '' ⇑(convex_hull π•œ) s
theorem affine_map.image_convex_hull {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring π•œ] [add_comm_group E] [add_comm_group F] [module π•œ E] [module π•œ F] (s : set E) (f : E →ᡃ[π•œ] F) :
⇑f '' ⇑(convex_hull π•œ) s = ⇑(convex_hull π•œ) (⇑f '' s)
theorem convex_hull_subset_affine_span {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (s : set E) :
⇑(convex_hull π•œ) s βŠ† ↑(affine_span π•œ s)
@[simp]
theorem affine_span_convex_hull {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (s : set E) :
affine_span π•œ (⇑(convex_hull π•œ) s) = affine_span π•œ s