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] :

closure_operator (set E)

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

Equations

convex_hull 𝕜 = closure_operator.mk₃ (λ (s : set E), ⋂ (t : set E) (hst : s ⊆ t) (ht : convex 𝕜 t), t) (convex 𝕜) _ _ _

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

⇑(convex_hull 𝕜) s ⊆ t ↔ 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] :

⇑(convex_hull 𝕜) set.univ = set.univ

@[simp]

theorem convex_hull_empty {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] :

⇑(convex_hull 𝕜) ∅ = ∅

@[simp]

theorem convex_hull_empty_iff {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :

⇑(convex_hull 𝕜) s = ∅ ↔ s = ∅

@[simp]

theorem convex_hull_nonempty_iff {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :

(⇑(convex_hull 𝕜) s).nonempty ↔ s.nonempty

@[protected]

theorem set.nonempty.convex_hull {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :

s.nonempty → (⇑(convex_hull 𝕜) s).nonempty

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