mathlib3 documentation

analysis.convex.join

Convex join #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 convex_join (𝕜 : Type u_2) {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s 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.

Equations
theorem mem_convex_join {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t : set E} {x : E} :
x convex_join 𝕜 s t (a : E) (H : a s) (b : E) (H : b t), x segment 𝕜 a b
theorem convex_join_comm {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s t : set E) :
convex_join 𝕜 s t = convex_join 𝕜 t s
theorem convex_join_mono {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s₁ s₂ t₁ t₂ : set E} (hs : s₁ s₂) (ht : t₁ t₂) :
convex_join 𝕜 s₁ t₁ convex_join 𝕜 s₂ t₂
theorem convex_join_mono_left {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {t s₁ s₂ : set E} (hs : s₁ s₂) :
convex_join 𝕜 s₁ t convex_join 𝕜 s₂ t
theorem convex_join_mono_right {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t₁ t₂ : set E} (ht : t₁ t₂) :
convex_join 𝕜 s t₁ convex_join 𝕜 s t₂
@[simp]
theorem convex_join_empty_left {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (t : set E) :
@[simp]
theorem convex_join_empty_right {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s : set E) :
@[simp]
theorem convex_join_singleton_left {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (t : set E) (x : E) :
convex_join 𝕜 {x} t = (y : E) (H : y t), segment 𝕜 x y
@[simp]
theorem convex_join_singleton_right {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s : set E) (y : E) :
convex_join 𝕜 s {y} = (x : E) (H : x s), segment 𝕜 x y
@[simp]
theorem convex_join_singletons {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {y : E} (x : E) :
convex_join 𝕜 {x} {y} = segment 𝕜 x y
@[simp]
theorem convex_join_union_left {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s₁ s₂ t : set E) :
convex_join 𝕜 (s₁ s₂) t = convex_join 𝕜 s₁ t convex_join 𝕜 s₂ t
@[simp]
theorem convex_join_union_right {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s t₁ t₂ : set E) :
convex_join 𝕜 s (t₁ t₂) = convex_join 𝕜 s t₁ convex_join 𝕜 s t₂
@[simp]
theorem convex_join_Union_left {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s : ι set E) (t : set E) :
convex_join 𝕜 ( (i : ι), s i) t = (i : ι), convex_join 𝕜 (s i) t
@[simp]
theorem convex_join_Union_right {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s : set E) (t : ι set E) :
convex_join 𝕜 s ( (i : ι), t i) = (i : ι), convex_join 𝕜 s (t i)
theorem segment_subset_convex_join {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t : set E} {x y : E} (hx : x s) (hy : y t) :
segment 𝕜 x y convex_join 𝕜 s t
theorem subset_convex_join_left {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t : set E} (h : t.nonempty) :
s convex_join 𝕜 s t
theorem subset_convex_join_right {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t : set E} (h : s.nonempty) :
t convex_join 𝕜 s t
theorem convex_join_subset {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t u : set E} (hs : s u) (ht : t u) (hu : convex 𝕜 u) :
convex_join 𝕜 s t u
theorem convex_join_subset_convex_hull {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (s t : set E) :
convex_join 𝕜 s t (convex_hull 𝕜) (s t)
theorem convex_join_assoc_aux {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (s t u : set E) :
convex_join 𝕜 (convex_join 𝕜 s t) u convex_join 𝕜 s (convex_join 𝕜 t u)
theorem convex_join_assoc {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (s t u : set E) :
convex_join 𝕜 (convex_join 𝕜 s t) u = convex_join 𝕜 s (convex_join 𝕜 t u)
theorem convex_join_left_comm {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (s t u : set E) :
convex_join 𝕜 s (convex_join 𝕜 t u) = convex_join 𝕜 t (convex_join 𝕜 s u)
theorem convex_join_right_comm {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (s t u : set E) :
convex_join 𝕜 (convex_join 𝕜 s t) u = convex_join 𝕜 (convex_join 𝕜 s u) t
theorem convex_join_convex_join_convex_join_comm {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (s t u v : set E) :
convex_join 𝕜 (convex_join 𝕜 s t) (convex_join 𝕜 u v) = convex_join 𝕜 (convex_join 𝕜 s u) (convex_join 𝕜 t v)
theorem convex_hull_insert {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hs : s.nonempty) :
theorem convex_join_segments {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (a b c d : E) :
convex_join 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convex_hull 𝕜) {a, b, c, d}
theorem convex_join_segment_singleton {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (a b c : E) :
convex_join 𝕜 (segment 𝕜 a b) {c} = (convex_hull 𝕜) {a, b, c}
theorem convex_join_singleton_segment {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (a b c : E) :
convex_join 𝕜 {a} (segment 𝕜 b c) = (convex_hull 𝕜) {a, b, c}
@[protected]
theorem convex.convex_join {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :
convex 𝕜 (convex_join 𝕜 s t)
@[protected]
theorem convex.convex_hull_union {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) (hs₀ : s.nonempty) (ht₀ : t.nonempty) :
(convex_hull 𝕜) (s t) = convex_join 𝕜 s t
theorem convex_hull_union {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E} (hs : s.nonempty) (ht : t.nonempty) :
(convex_hull 𝕜) (s t) = convex_join 𝕜 ((convex_hull 𝕜) s) ((convex_hull 𝕜) t)