Documentation

Mathlib.Analysis.Convex.Hull

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.

@[simp]
theorem convexHull_isClosed (๐•œ : Type u_1) {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] (s : Set E) :
(convexHull ๐•œ).IsClosed s = Convex ๐•œ s
def convexHull (๐•œ : Type u_1) {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] :

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

Equations
Instances For
    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} :
    s โŠ† t โ†’ 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 convexHull_eq_self {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {s : Set E} :
    (convexHull ๐•œ) s = s โ†” Convex ๐•œ s
    theorem Convex.convexHull_eq {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [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} [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] :
    @[simp]
    theorem convexHull_empty_iff {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {s : Set E} :
    @[simp]
    theorem convexHull_nonempty_iff {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {s : Set E} :
    ((convexHull ๐•œ) s).Nonempty โ†” s.Nonempty
    theorem Set.Nonempty.convexHull {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [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} [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.image_convexHull {๐•œ : 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) :
    f '' (convexHull ๐•œ) s = (convexHull ๐•œ) (f '' s)
    theorem LinearMap.image_convexHull {๐•œ : 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) :
    โ‡‘f '' (convexHull ๐•œ) s = (convexHull ๐•œ) (โ‡‘f '' 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] (f : E โ†’แตƒ[๐•œ] F) (s : Set E) :
    โ‡‘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
    theorem convexHull_vadd {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (x : E) (s : Set E) :
    (convexHull ๐•œ) (x +แตฅ s) = x +แตฅ (convexHull ๐•œ) s