Convex hull

This file defines the convex hull of a set s in a module. convexHull 𝕜 s is the smallest convex set containing s. In order theory speak, this is a closure operator.

Implementation notes

convexHull is defined as a closure operator. This gives access to the ClosureOperator API while the impact on writing code is minimal as convexHull 𝕜 s is automatically elaborated as (convexHull 𝕜) s.

def convexHull (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ClosureOperator (Set E)

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

Equations

• One or more equations did not get rendered due to their size.

theorem subset_convexHull (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) : s ⊆ ↑(convexHull 𝕜) s

theorem convex_convexHull (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) : Convex 𝕜 (↑(convexHull 𝕜) s)

theorem convexHull_eq_iInter (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) : ↑(convexHull 𝕜) s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : Convex 𝕜 t), t

theorem mem_convexHull_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} : x ∈ ↑(convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t

theorem convexHull_min {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (hst : s ⊆ t) (ht : Convex 𝕜 t) : ↑(convexHull 𝕜) s ⊆ t

theorem Convex.convexHull_subset_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (ht : Convex 𝕜 t) : ↑(convexHull 𝕜) s ⊆ t ↔ s ⊆ t

theorem convexHull_mono {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (hst : s ⊆ t) : ↑(convexHull 𝕜) s ⊆ ↑(convexHull 𝕜) t

theorem Convex.convexHull_eq {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Convex 𝕜 s → ↑(convexHull 𝕜) s = s

@[simp]

theorem convexHull_univ {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ↑(convexHull 𝕜) Set.univ = Set.univ

@[simp]

theorem convexHull_empty {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ↑(convexHull 𝕜) ∅ = ∅

@[simp]

theorem convexHull_empty_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : ↑(convexHull 𝕜) s = ∅ ↔ s = ∅

@[simp]

theorem convexHull_nonempty_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Set.Nonempty (↑(convexHull 𝕜) s) ↔ Set.Nonempty s

theorem Set.Nonempty.convexHull {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Set.Nonempty s → Set.Nonempty (↑(convexHull 𝕜) s)

Alias of the reverse direction of convexHull_nonempty_iff.

theorem segment_subset_convexHull {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) : segment 𝕜 x y ⊆ ↑(convexHull 𝕜) s

@[simp]

theorem convexHull_singleton {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) : ↑(convexHull 𝕜) {x} = {x}

@[simp]

theorem convexHull_zero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ↑(convexHull 𝕜) 0 = 0

@[simp]

theorem convexHull_pair {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) (y : E) : ↑(convexHull 𝕜) {x, y} = segment 𝕜 x y

theorem convexHull_convexHull_union_left {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) : ↑(convexHull 𝕜) (↑(convexHull 𝕜) s ∪ t) = ↑(convexHull 𝕜) (s ∪ t)

theorem convexHull_convexHull_union_right {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) : ↑(convexHull 𝕜) (s ∪ ↑(convexHull 𝕜) t) = ↑(convexHull 𝕜) (s ∪ t)

theorem Convex.convex_remove_iff_not_mem_convexHull_remove {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (x : E) : Convex 𝕜 (s \ {x}) ↔ ¬x ∈ ↑(convexHull 𝕜) (s \ {x})

theorem IsLinearMap.convexHull_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {f : E → F} (hf : IsLinearMap 𝕜 f) (s : Set E) : ↑(convexHull 𝕜) (f '' s) = f '' ↑(convexHull 𝕜) s

theorem LinearMap.convexHull_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (s : Set E) : ↑(convexHull 𝕜) (↑f '' s) = ↑f '' ↑(convexHull 𝕜) s

theorem convexHull_smul {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (a : 𝕜) (s : Set E) : ↑(convexHull 𝕜) (a • s) = a • ↑(convexHull 𝕜) s

theorem AffineMap.image_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (s : Set E) (f : E →ᵃ[𝕜] F) : ↑f '' ↑(convexHull 𝕜) s = ↑(convexHull 𝕜) (↑f '' s)

theorem convexHull_subset_affineSpan {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : ↑(convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)

@[simp]

theorem affineSpan_convexHull {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : affineSpan 𝕜 (↑(convexHull 𝕜) s) = affineSpan 𝕜 s

theorem convexHull_neg {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : ↑(convexHull 𝕜) (-s) = -↑(convexHull 𝕜) s