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.

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.

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} (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