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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ClosureOperator (Set E)

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

Equations

• convexHull 𝕜 = ClosureOperator.ofCompletePred (Convex 𝕜) ⋯

@[simp]

theorem convexHull_isClosed (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) : (convexHull 𝕜).IsClosed s = Convex 𝕜 s

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

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

theorem convexHull_eq_iInter (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [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} [Semiring 𝕜] [PartialOrder 𝕜] [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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} : s ⊆ t → Convex 𝕜 t → (convexHull 𝕜) s ⊆ t

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

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

theorem convexHull_eq_self {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : (convexHull 𝕜) s = s ↔ Convex 𝕜 s

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

Alias of the reverse direction of convexHull_eq_self.

@[simp]

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

@[simp]

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

@[simp]

theorem convexHull_eq_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : (convexHull 𝕜) s = ∅ ↔ s = ∅

@[simp]

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

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

Alias of the reverse direction of convexHull_nonempty_iff.

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

@[simp]

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

@[simp]

theorem convexHull_eq_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} : (convexHull 𝕜) s = {x} ↔ s = {x}

@[simp]

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

@[simp]

theorem convexHull_eq_zero {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : (convexHull 𝕜) s = 0 ↔ s = 0

@[simp]

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

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

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

theorem Convex.convex_remove_iff_notMem_convexHull_remove {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (x : E) : Convex 𝕜 (s \ {x}) ↔ x ∉ (convexHull 𝕜) (s \ {x})

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

theorem LinearMap.image_convexHull {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (s : Set E) : ⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)

theorem convexHull_add_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} : (convexHull 𝕜) (s + t) ⊆ (convexHull 𝕜) s + (convexHull 𝕜) t

theorem convexHull_smul {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [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} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (s : Set E) : ⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)

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

@[simp]

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

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

theorem convexHull_vadd {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (s : Set E) : (convexHull 𝕜) (x +ᵥ s) = x +ᵥ (convexHull 𝕜) s