Documentation

Mathlib.Analysis.Convex.Join

Convex join #

This file defines the convex join of two sets. The convex join of s and t is the union of the segments with one end in s and the other in t. This is notably a useful gadget to deal with convex hulls of finite sets.

def convexJoin (𝕜 : Type u_2) {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) :
Set E

The join of two sets is the union of the segments joining them. This can be interpreted as the topological join, but within the original space.

Instances For
    theorem mem_convexJoin {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} {x : E} :
    x ∈ convexJoin 𝕜 s t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ x ∈ segment 𝕜 a b
    theorem convexJoin_comm {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) :
    convexJoin 𝕜 s t = convexJoin 𝕜 t s
    theorem convexJoin_mono {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
    convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂
    theorem convexJoin_mono_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {t : Set E} {s₁ : Set E} {s₂ : Set E} (hs : s₁ ⊆ s₂) :
    convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t
    theorem convexJoin_mono_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t₁ : Set E} {t₂ : Set E} (ht : t₁ ⊆ t₂) :
    convexJoin 𝕜 s t₁ ⊆ convexJoin 𝕜 s t₂
    @[simp]
    theorem convexJoin_empty_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) :
    @[simp]
    theorem convexJoin_empty_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) :
    @[simp]
    theorem convexJoin_singleton_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (t : Set E) (x : E) :
    convexJoin 𝕜 {x} t = ⋃ (y : E) (_ : y ∈ t), segment 𝕜 x y
    @[simp]
    theorem convexJoin_singleton_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (y : E) :
    convexJoin 𝕜 s {y} = ⋃ (x : E) (_ : x ∈ s), segment 𝕜 x y
    theorem convexJoin_singletons {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {y : E} (x : E) :
    convexJoin 𝕜 {x} {y} = segment 𝕜 x y
    @[simp]
    theorem convexJoin_union_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s₁ : Set E) (s₂ : Set E) (t : Set E) :
    convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
    @[simp]
    theorem convexJoin_union_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t₁ : Set E) (t₂ : Set E) :
    convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂
    @[simp]
    theorem convexJoin_iUnion_left {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : ι → Set E) (t : Set E) :
    convexJoin 𝕜 (⋃ (i : ι), s i) t = ⋃ (i : ι), convexJoin 𝕜 (s i) t
    @[simp]
    theorem convexJoin_iUnion_right {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : ι → Set E) :
    convexJoin 𝕜 s (⋃ (i : ι), t i) = ⋃ (i : ι), convexJoin 𝕜 s (t i)
    theorem segment_subset_convexJoin {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ t) :
    segment 𝕜 x y ⊆ convexJoin 𝕜 s t
    theorem subset_convexJoin_left {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (h : Set.Nonempty t) :
    s ⊆ convexJoin 𝕜 s t
    theorem subset_convexJoin_right {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (h : Set.Nonempty s) :
    t ⊆ convexJoin 𝕜 s t
    theorem convexJoin_subset {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} {u : Set E} (hs : s ⊆ u) (ht : t ⊆ u) (hu : Convex 𝕜 u) :
    convexJoin 𝕜 s t ⊆ u
    theorem convexJoin_subset_convexHull {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) (t : Set E) :
    convexJoin 𝕜 s t ⊆ ↑(convexHull 𝕜) (s ∪ t)
    theorem convexJoin_assoc_aux {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)
    theorem convexJoin_assoc {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)
    theorem convexJoin_left_comm {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :
    convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)
    theorem convexJoin_right_comm {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t
    theorem convexJoin_convexJoin_convexJoin_comm {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (t : Set E) (u : Set E) (v : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)
    theorem Convex.convexJoin {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) :
    Convex 𝕜 (convexJoin 𝕜 s t)
    theorem Convex.convexHull_union {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hs₀ : Set.Nonempty s) (ht₀ : Set.Nonempty t) :
    ↑(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 s t
    theorem convexHull_union {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Set.Nonempty s) (ht : Set.Nonempty t) :
    ↑(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 (↑(convexHull 𝕜) s) (↑(convexHull 𝕜) t)
    theorem convexHull_insert {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} (hs : Set.Nonempty s) :
    ↑(convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} (↑(convexHull 𝕜) s)
    theorem convexJoin_segments {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) (d : E) :
    convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = ↑(convexHull 𝕜) {a, b, c, d}
    theorem convexJoin_segment_singleton {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :
    convexJoin 𝕜 (segment 𝕜 a b) {c} = ↑(convexHull 𝕜) {a, b, c}
    theorem convexJoin_singleton_segment {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :
    convexJoin 𝕜 {a} (segment 𝕜 b c) = ↑(convexHull 𝕜) {a, b, c}