Mathlib.Analysis.Convex.Hull

convexHull definition

: ClosureOperator (Set E)

Full source

/-- The convex hull of a set `s` is the minimal convex set that includes `s`. -/
@[simps! isClosed]
def convexHull : ClosureOperator (Set E) := .ofCompletePred (Convex 𝕜) fun _ ↦ convex_sInter

Convex hull of a set

Informal description

The convex hull of a set $s$ in a module over a scalar ring $\mathbb{K}$ is the smallest convex set containing $s$, defined as the intersection of all convex sets that include $s$.

subset_convexHull theorem

: s ⊆ convexHull 𝕜 s

Full source

theorem subset_convexHull : s ⊆ convexHull 𝕜 s :=
  (convexHull 𝕜).le_closure s

Set is Subset of its Convex Hull

Informal description

For any set $s$ in a module over a scalar ring $\mathbb{K}$, the set $s$ is a subset of its convex hull, i.e., $s \subseteq \text{convexHull}_{\mathbb{K}}(s)$.

convex_convexHull theorem

: Convex 𝕜 (convexHull 𝕜 s)

Full source

theorem convex_convexHull : Convex 𝕜 (convexHull 𝕜 s) := (convexHull 𝕜).isClosed_closure s

Convexity of the Convex Hull

Informal description

For any set $s$ in a module over a scalar ring $\mathbb{K}$, the convex hull $\text{convexHull}_{\mathbb{K}}(s)$ is a convex set.

convexHull_eq_iInter theorem

: convexHull 𝕜 s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : Convex 𝕜 t), t

Full source

theorem convexHull_eq_iInter : convexHull 𝕜 s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : Convex 𝕜 t), t := by
  simp [convexHull, iInter_subtype, iInter_and]

Convex Hull as Intersection of All Containing Convex Sets

Informal description

The convex hull of a set $s$ in a module over a scalar ring $\mathbb{K}$ is equal to the intersection of all convex sets $t$ that contain $s$. That is, \[ \text{convexHull}_{\mathbb{K}}(s) = \bigcap_{\substack{t \subseteq E \\ s \subseteq t \\ \text{Convex}_{\mathbb{K}}(t)}} t. \]

mem_convexHull_iff theorem

: x ∈ convexHull 𝕜 s ↔ ∀ t, s ⊆ t → Convex 𝕜 t → x ∈ t

Full source

theorem mem_convexHull_iff : x ∈ convexHull 𝕜 sx ∈ convexHull 𝕜 s ↔ ∀ t, s ⊆ t → Convex 𝕜 t → x ∈ t := by
  simp_rw [convexHull_eq_iInter, mem_iInter]

Characterization of Membership in Convex Hull via Containing Convex Sets

Informal description

An element $x$ belongs to the convex hull of a set $s$ in a module over a scalar ring $\mathbb{K}$ if and only if for every convex set $t$ containing $s$, $x$ is also in $t$. That is, \[ x \in \text{convexHull}_{\mathbb{K}}(s) \leftrightarrow \forall t, (s \subseteq t \land \text{Convex}_{\mathbb{K}}(t)) \to x \in t. \]

convexHull_min theorem

: s ⊆ t → Convex 𝕜 t → convexHull 𝕜 s ⊆ t

Full source

theorem convexHull_min : s ⊆ t → Convex 𝕜 t → convexHullconvexHull 𝕜 s ⊆ t := (convexHull 𝕜).closure_min

Minimality of the Convex Hull: $\text{convexHull}_{\mathbb{K}}(s) \subseteq t$ for $s \subseteq t$ and $t$ convex

Informal description

For any subset $s$ of a module over a scalar ring $\mathbb{K}$, if $s$ is contained in a convex set $t$, then the convex hull of $s$ is also contained in $t$.

Convex.convexHull_subset_iff theorem

(ht : Convex 𝕜 t) : convexHull 𝕜 s ⊆ t ↔ s ⊆ t

Full source

theorem Convex.convexHull_subset_iff (ht : Convex 𝕜 t) : convexHullconvexHull 𝕜 s ⊆ tconvexHull 𝕜 s ⊆ t ↔ s ⊆ t :=
  (show (convexHull 𝕜).IsClosed t from ht).closure_le_iff

Characterization of Convex Hull Containment in a Convex Set: $\text{convexHull}_\mathbb{K}(s) \subseteq t \leftrightarrow s \subseteq t$ when $t$ is convex

Informal description

Let $s$ and $t$ be sets in a module over a scalar ring $\mathbb{K}$, and suppose $t$ is convex. Then the convex hull of $s$ is contained in $t$ if and only if $s$ is contained in $t$. In other words, $\text{convexHull}_\mathbb{K}(s) \subseteq t \leftrightarrow s \subseteq t$.

convexHull_mono theorem

(hst : s ⊆ t) : convexHull 𝕜 s ⊆ convexHull 𝕜 t

Full source

@[mono, gcongr]
theorem convexHull_mono (hst : s ⊆ t) : convexHullconvexHull 𝕜 s ⊆ convexHull 𝕜 t :=
  (convexHull 𝕜).monotone hst

Monotonicity of Convex Hull: $s \subseteq t \implies \text{convexHull}(\mathbb{K}, s) \subseteq \text{convexHull}(\mathbb{K}, t)$

Informal description

For any two sets $s$ and $t$ in a module over a scalar ring $\mathbb{K}$, if $s$ is a subset of $t$, then the convex hull of $s$ is a subset of the convex hull of $t$.

convexHull_eq_self theorem

: convexHull 𝕜 s = s ↔ Convex 𝕜 s

Full source

lemma convexHull_eq_self : convexHullconvexHull 𝕜 s = s ↔ Convex 𝕜 s := (convexHull 𝕜).isClosed_iff.symm

Convex Hull Equals Set if and only if Set is Convex

Informal description

For a set $s$ in a module over a scalar ring $\mathbb{K}$, the convex hull of $s$ equals $s$ itself if and only if $s$ is convex. In other words, $\text{convexHull}_{\mathbb{K}}(s) = s \leftrightarrow \text{Convex}_{\mathbb{K}}(s)$.

convexHull_univ theorem

: convexHull 𝕜 (univ : Set E) = univ

Full source

@[simp]
theorem convexHull_univ : convexHull 𝕜 (univ : Set E) = univ :=
  ClosureOperator.closure_top (convexHull 𝕜)

Convex Hull of Universal Set is Universal Set

Informal description

For any scalar ring $\mathbb{K}$ and module $E$ over $\mathbb{K}$, the convex hull of the universal set in $E$ is equal to the universal set itself, i.e., $\text{convexHull}_{\mathbb{K}}(E) = E$.

convexHull_empty theorem

: convexHull 𝕜 (∅ : Set E) = ∅

Full source

@[simp]
theorem convexHull_empty : convexHull 𝕜 (∅ : Set E) = ∅ :=
  convex_empty.convexHull_eq

Convex Hull of Empty Set is Empty

Informal description

The convex hull of the empty set in a module $E$ over a scalar ring $\mathbb{K}$ is the empty set, i.e., $\text{convexHull}_{\mathbb{K}}(\emptyset) = \emptyset$.

convexHull_empty_iff theorem

: convexHull 𝕜 s = ∅ ↔ s = ∅

Full source

@[simp]
theorem convexHull_empty_iff : convexHullconvexHull 𝕜 s = ∅ ↔ s = ∅ := by
  constructor
  · intro h
    rw [← Set.subset_empty_iff, ← h]
    exact subset_convexHull 𝕜 _
  · rintro rfl
    exact convexHull_empty

Convex Hull is Empty if and only if Set is Empty

Informal description

For any set $s$ in a module over a scalar ring $\mathbb{K}$, the convex hull of $s$ is empty if and only if $s$ itself is empty, i.e., $\text{convexHull}_{\mathbb{K}}(s) = \emptyset \leftrightarrow s = \emptyset$.

convexHull_nonempty_iff theorem

: (convexHull 𝕜 s).Nonempty ↔ s.Nonempty

Full source

@[simp]
theorem convexHull_nonempty_iff : (convexHull 𝕜 s).Nonempty ↔ s.Nonempty := by
  rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]
  exact not_congr convexHull_empty_iff

Nonempty Convex Hull Characterization: $\text{convexHull}_{\mathbb{K}}(s) \neq \emptyset \leftrightarrow s \neq \emptyset$

Informal description

For any set $s$ in a module over a scalar ring $\mathbb{K}$, the convex hull of $s$ is nonempty if and only if $s$ itself is nonempty, i.e., $\text{convexHull}_{\mathbb{K}}(s) \neq \emptyset \leftrightarrow s \neq \emptyset$.

segment_subset_convexHull theorem

(hx : x ∈ s) (hy : y ∈ s) : segment 𝕜 x y ⊆ convexHull 𝕜 s

Full source

theorem segment_subset_convexHull (hx : x ∈ s) (hy : y ∈ s) : segmentsegment 𝕜 x y ⊆ convexHull 𝕜 s :=
  (convex_convexHull _ _).segment_subset (subset_convexHull _ _ hx) (subset_convexHull _ _ hy)

Segment is Subset of Convex Hull

Informal description

For any two points $x$ and $y$ in a set $s$ in a module over a scalar ring $\mathbb{K}$, the segment connecting $x$ and $y$ is contained in the convex hull of $s$, i.e., $\text{segment}_{\mathbb{K}}(x, y) \subseteq \text{convexHull}_{\mathbb{K}}(s)$.

convexHull_singleton theorem

(x : E) : convexHull 𝕜 ({ x } : Set E) = { x }

Full source

@[simp]
theorem convexHull_singleton (x : E) : convexHull 𝕜 ({x} : Set E) = {x} :=
  (convex_singleton x).convexHull_eq

Convex Hull of a Singleton Set is the Singleton Itself

Informal description

For any element $x$ in a module $E$ over a scalar ring $\mathbb{K}$, the convex hull of the singleton set $\{x\}$ is equal to $\{x\}$ itself.

convexHull_zero theorem

: convexHull 𝕜 (0 : Set E) = 0

Full source

@[simp]
theorem convexHull_zero : convexHull 𝕜 (0 : Set E) = 0 :=
  convexHull_singleton 0

Convex Hull of Zero Set is Zero

Informal description

The convex hull of the zero set $\{0\}$ in a module $E$ over a scalar ring $\mathbb{K}$ is equal to $\{0\}$ itself, i.e., $\text{convexHull}_\mathbb{K}(\{0\}) = \{0\}$.

convexHull_pair theorem

[IsOrderedRing 𝕜] (x y : E) : convexHull 𝕜 { x, y } = segment 𝕜 x y

Full source

@[simp]
theorem convexHull_pair [IsOrderedRing 𝕜] (x y : E) : convexHull 𝕜 {x, y} = segment 𝕜 x y := by
  refine (convexHull_min ?_ <| convex_segment _ _).antisymm
    (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)
  rw [insert_subset_iff, singleton_subset_iff]
  exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩

Convex Hull of Two Points Equals Their Connecting Segment

Informal description

For any ordered ring $\mathbb{K}$ and any two points $x$ and $y$ in a module $E$ over $\mathbb{K}$, the convex hull of the two-point set $\{x, y\}$ is equal to the segment connecting $x$ and $y$, i.e., \[ \text{convexHull}_\mathbb{K}(\{x, y\}) = \text{segment}_\mathbb{K}(x, y). \]

convexHull_convexHull_union_left theorem

(s t : Set E) : convexHull 𝕜 (convexHull 𝕜 s ∪ t) = convexHull 𝕜 (s ∪ t)

Full source

theorem convexHull_convexHull_union_left (s t : Set E) :
    convexHull 𝕜 (convexHullconvexHull 𝕜 s ∪ t) = convexHull 𝕜 (s ∪ t) :=
  ClosureOperator.closure_sup_closure_left _ _ _

Convex Hull of Union with Left Convex Hull: $\text{convexHull}_\mathbb{K}(\text{convexHull}_\mathbb{K}(s) \cup t) = \text{convexHull}_\mathbb{K}(s \cup t)$

Informal description

For any two sets $s$ and $t$ in a module $E$ over a scalar ring $\mathbb{K}$, the convex hull of the union of the convex hull of $s$ and $t$ is equal to the convex hull of the union of $s$ and $t$, i.e., \[ \text{convexHull}_\mathbb{K}(\text{convexHull}_\mathbb{K}(s) \cup t) = \text{convexHull}_\mathbb{K}(s \cup t). \]

convexHull_convexHull_union_right theorem

(s t : Set E) : convexHull 𝕜 (s ∪ convexHull 𝕜 t) = convexHull 𝕜 (s ∪ t)

Full source

theorem convexHull_convexHull_union_right (s t : Set E) :
    convexHull 𝕜 (s ∪ convexHull 𝕜 t) = convexHull 𝕜 (s ∪ t) :=
  ClosureOperator.closure_sup_closure_right _ _ _

Convex Hull of Union with Right Convex Hull: $\text{convexHull}_\mathbb{K}(s \cup \text{convexHull}_\mathbb{K}(t)) = \text{convexHull}_\mathbb{K}(s \cup t)$

Informal description

For any two sets $s$ and $t$ in a module $E$ over a scalar ring $\mathbb{K}$, the convex hull of the union of $s$ and the convex hull of $t$ is equal to the convex hull of the union of $s$ and $t$, i.e., \[ \text{convexHull}_\mathbb{K}(s \cup \text{convexHull}_\mathbb{K}(t)) = \text{convexHull}_\mathbb{K}(s \cup t). \]

Convex.convex_remove_iff_not_mem_convexHull_remove theorem

{s : Set E} (hs : Convex 𝕜 s) (x : E) : Convex 𝕜 (s \ { x }) ↔ x ∉ convexHull 𝕜 (s \ { x })

Full source

theorem Convex.convex_remove_iff_not_mem_convexHull_remove {s : Set E} (hs : Convex 𝕜 s) (x : E) :
    ConvexConvex 𝕜 (s \ {x}) ↔ x ∉ convexHull 𝕜 (s \ {x}) := by
  constructor
  · rintro hsx hx
    rw [hsx.convexHull_eq] at hx
    exact hx.2 (mem_singleton _)
  rintro hx
  suffices h : s \ {x} = convexHull 𝕜 (s \ {x}) by
    rw [h]
    exact convex_convexHull 𝕜 _
  exact
    Subset.antisymm (subset_convexHull 𝕜 _) fun y hy =>
      ⟨convexHull_min diff_subset hs hy, by
        rintro (rfl : y = x)
        exact hx hy⟩

Convexity of Set Difference from a Singleton: $s \setminus \{x\}$ is convex iff $x \notin \text{convexHull}_\mathbb{K}(s \setminus \{x\})$

Informal description

Let $s$ be a convex set in a module $E$ over a scalar ring $\mathbb{K}$, and let $x \in E$. Then the set difference $s \setminus \{x\}$ is convex if and only if $x$ does not belong to the convex hull of $s \setminus \{x\}$.

IsLinearMap.image_convexHull theorem

{f : E → F} (hf : IsLinearMap 𝕜 f) (s : Set E) : f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s)

Full source

theorem IsLinearMap.image_convexHull {f : E → F} (hf : IsLinearMap 𝕜 f) (s : Set E) :
    f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s) :=
  Set.Subset.antisymm
    (image_subset_iff.2 <|
      convexHull_min (image_subset_iff.1 <| subset_convexHull 𝕜 _)
        ((convex_convexHull 𝕜 _).is_linear_preimage hf))
    (convexHull_min (image_subset _ (subset_convexHull 𝕜 s)) <|
      (convex_convexHull 𝕜 s).is_linear_image hf)

Linear Image of Convex Hull Equals Convex Hull of Linear Image

Informal description

Let $E$ and $F$ be modules over a scalar ring $\mathbb{K}$, and let $f \colon E \to F$ be a $\mathbb{K}$-linear map. For any subset $s \subseteq E$, the image of the convex hull of $s$ under $f$ equals the convex hull of the image of $s$ under $f$. In symbols: \[ f(\text{convexHull}_\mathbb{K}(s)) = \text{convexHull}_\mathbb{K}(f(s)). \]

LinearMap.image_convexHull theorem

(f : E →ₗ[𝕜] F) (s : Set E) : f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s)

Full source

theorem LinearMap.image_convexHull (f : E →ₗ[𝕜] F) (s : Set E) :
    f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s) :=
  f.isLinear.image_convexHull s

Linear Image of Convex Hull Equals Convex Hull of Linear Image

Informal description

Let $E$ and $F$ be modules over a scalar ring $\mathbb{K}$, and let $f \colon E \to F$ be a $\mathbb{K}$-linear map. For any subset $s \subseteq E$, the image of the convex hull of $s$ under $f$ equals the convex hull of the image of $s$ under $f$. In symbols: \[ f(\text{convexHull}_\mathbb{K}(s)) = \text{convexHull}_\mathbb{K}(f(s)). \]

convexHull_add_subset theorem

{s t : Set E} : convexHull 𝕜 (s + t) ⊆ convexHull 𝕜 s + convexHull 𝕜 t

Full source

theorem convexHull_add_subset {s t : Set E} :
    convexHullconvexHull 𝕜 (s + t) ⊆ convexHull 𝕜 s + convexHull 𝕜 t :=
  convexHull_min (add_subset_add (subset_convexHull _ _) (subset_convexHull _ _))
    (Convex.add (convex_convexHull 𝕜 s) (convex_convexHull 𝕜 t))

Convex Hull of Minkowski Sum is Subset of Sum of Convex Hulls

Informal description

For any two subsets $s$ and $t$ of a module $E$ over a scalar ring $\mathbb{K}$, the convex hull of their Minkowski sum $s + t$ is contained in the Minkowski sum of their convex hulls, i.e., $$\text{convexHull}_{\mathbb{K}}(s + t) \subseteq \text{convexHull}_{\mathbb{K}}(s) + \text{convexHull}_{\mathbb{K}}(t).$$

convexHull_smul theorem

(a : 𝕜) (s : Set E) : convexHull 𝕜 (a • s) = a • convexHull 𝕜 s

Full source

theorem convexHull_smul (a : 𝕜) (s : Set E) : convexHull 𝕜 (a • s) = a • convexHull 𝕜 s :=
  (LinearMap.lsmul _ _ a).image_convexHull _ |>.symm

Scalar Multiplication Commutes with Convex Hull

Informal description

For any scalar $a$ in a scalar ring $\mathbb{K}$ and any subset $s$ of a module $E$ over $\mathbb{K}$, the convex hull of the scaled set $a \cdot s$ is equal to the scaled convex hull of $s$, i.e., \[ \text{convexHull}_{\mathbb{K}}(a \cdot s) = a \cdot \text{convexHull}_{\mathbb{K}}(s). \]

AffineMap.image_convexHull theorem

(f : E →ᵃ[𝕜] F) (s : Set E) : f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s)

Full source

theorem AffineMap.image_convexHull (f : E →ᵃ[𝕜] F) (s : Set E) :
    f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s) := by
  apply Set.Subset.antisymm
  · rw [Set.image_subset_iff]
    refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
    rw [← Set.image_subset_iff]
    exact subset_convexHull 𝕜 (f '' s)
  · exact convexHull_min (Set.image_subset _ (subset_convexHull 𝕜 s))
      ((convex_convexHull 𝕜 s).affine_image f)

Affine Image of Convex Hull Equals Convex Hull of Affine Image

Informal description

For any affine map $f \colon E \to F$ between modules over a scalar ring $\mathbb{K}$ and any subset $s \subseteq E$, the image of the convex hull of $s$ under $f$ equals the convex hull of the image of $s$ under $f$. In symbols: \[ f(\text{convexHull}_{\mathbb{K}}(s)) = \text{convexHull}_{\mathbb{K}}(f(s)). \]

convexHull_subset_affineSpan theorem

(s : Set E) : convexHull 𝕜 s ⊆ (affineSpan 𝕜 s : Set E)

Full source

theorem convexHull_subset_affineSpan (s : Set E) : convexHullconvexHull 𝕜 s ⊆ (affineSpan 𝕜 s : Set E) :=
  convexHull_min (subset_affineSpan 𝕜 s) (affineSpan 𝕜 s).convex

Convex Hull is Contained in Affine Span

Informal description

For any subset $s$ of a module $E$ over a scalar ring $\mathbb{K}$, the convex hull of $s$ is contained in the affine span of $s$. In symbols: \[ \text{convexHull}_{\mathbb{K}}(s) \subseteq \text{affineSpan}_{\mathbb{K}}(s). \]

affineSpan_convexHull theorem

(s : Set E) : affineSpan 𝕜 (convexHull 𝕜 s) = affineSpan 𝕜 s

Full source

@[simp]
theorem affineSpan_convexHull (s : Set E) : affineSpan 𝕜 (convexHull 𝕜 s) = affineSpan 𝕜 s := by
  refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
  rw [affineSpan_le]
  exact convexHull_subset_affineSpan s

Affine Span of Convex Hull Equals Affine Span

Informal description

For any subset $s$ of a module $E$ over a scalar ring $\mathbb{K}$, the affine span of the convex hull of $s$ is equal to the affine span of $s$. In symbols: \[ \text{affineSpan}_{\mathbb{K}}(\text{convexHull}_{\mathbb{K}}(s)) = \text{affineSpan}_{\mathbb{K}}(s). \]

convexHull_neg theorem

(s : Set E) : convexHull 𝕜 (-s) = -convexHull 𝕜 s

Full source

theorem convexHull_neg (s : Set E) : convexHull 𝕜 (-s) = -convexHull 𝕜 s := by
  simp_rw [← image_neg_eq_neg]
  exact AffineMap.image_convexHull (-1) _ |>.symm

Negation Commutes with Convex Hull

Informal description

For any subset $s$ of a module $E$ over a scalar ring $\mathbb{K}$, the convex hull of the negation of $s$ equals the negation of the convex hull of $s$. In symbols: \[ \text{convexHull}_{\mathbb{K}}(-s) = -\text{convexHull}_{\mathbb{K}}(s). \]

convexHull_vadd theorem

(x : E) (s : Set E) : convexHull 𝕜 (x +ᵥ s) = x +ᵥ convexHull 𝕜 s

Full source

lemma convexHull_vadd (x : E) (s : Set E) : convexHull 𝕜 (x +ᵥ s) = x +ᵥ convexHull 𝕜 s :=
  (AffineEquiv.constVAdd 𝕜 _ x).toAffineMap.image_convexHull s |>.symm

Convex Hull of Translated Set Equals Translation of Convex Hull

Informal description

For any vector $x$ in a module $E$ over a scalar ring $\mathbb{K}$ and any subset $s \subseteq E$, the convex hull of the translation of $s$ by $x$ is equal to the translation of the convex hull of $s$ by $x$. In symbols: \[ \text{convexHull}_{\mathbb{K}}(x + s) = x + \text{convexHull}_{\mathbb{K}}(s). \]

Implementation notes