mathlib3 documentation

analysis.convex.hull

Convex hull #

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

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_eq_Inter (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (s : set E) :
⇑(convex_hull π•œ) s = β‹‚ (t : set E) (hst : s βŠ† t) (ht : convex π•œ t), t
theorem mem_convex_hull_iff {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} {x : E} :
x ∈ ⇑(convex_hull π•œ) s ↔ βˆ€ (t : set E), s βŠ† t β†’ convex π•œ t β†’ x ∈ t
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.convex_hull_subset_iff {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s t : set E} (ht : convex π•œ 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} :
@[protected]
theorem set.nonempty.convex_hull {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} :

Alias of the reverse direction of convex_hull_nonempty_iff.

theorem segment_subset_convex_hull {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
segment π•œ x y βŠ† ⇑(convex_hull π•œ) s
@[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}
@[simp]
theorem convex_hull_zero {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
⇑(convex_hull π•œ) 0 = 0
@[simp]
theorem convex_hull_pair {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (x y : E) :
⇑(convex_hull π•œ) {x, y} = segment π•œ x y
theorem convex_hull_convex_hull_union_left {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (s t : set E) :
⇑(convex_hull π•œ) (⇑(convex_hull π•œ) s βˆͺ t) = ⇑(convex_hull π•œ) (s βˆͺ t)
theorem convex_hull_convex_hull_union_right {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (s t : set E) :
⇑(convex_hull π•œ) (s βˆͺ ⇑(convex_hull π•œ) t) = ⇑(convex_hull π•œ) (s βˆͺ t)
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.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 convex_hull_smul {π•œ : Type u_1} {E : Type u_2} [ordered_comm_semiring π•œ] [add_comm_monoid E] [module π•œ E] (a : π•œ) (s : set E) :
⇑(convex_hull π•œ) (a β€’ s) = a β€’ ⇑(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
theorem convex_hull_neg {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (s : set E) :
⇑(convex_hull π•œ) (-s) = -⇑(convex_hull π•œ) s