mathlib3 documentation

analysis.convex.basic

Convex sets and functions in vector spaces #

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

In a 𝕜-vector space, we define the following objects and properties.

We also provide various equivalent versions of the definitions above, prove that some specific sets are convex.

TODO #

Generalize all this file to affine spaces.

Convexity of sets #

def convex (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (s : set E) :
Prop

Convexity of sets.

Equations
theorem convex.star_convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s : set E} {x : E} (hs : convex 𝕜 s) (hx : x s) :
star_convex 𝕜 x s
theorem convex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s : set E} :
convex 𝕜 s ⦃x : E⦄, x s ⦃y : E⦄, y s segment 𝕜 x y s
theorem convex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s : set E} (h : convex 𝕜 s) {x y : E} (hx : x s) (hy : y s) :
segment 𝕜 x y s
theorem convex.open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s : set E} (h : convex 𝕜 s) {x y : E} (hx : x s) (hy : y s) :
open_segment 𝕜 x y s
theorem convex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s : set E} :
convex 𝕜 s ⦃a b : 𝕜⦄, 0 a 0 b a + b = 1 a s + b s s

Alternative definition of set convexity, in terms of pointwise set operations.

theorem convex.set_combo_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s : set E} :
convex 𝕜 s ⦃a b : 𝕜⦄, 0 a 0 b a + b = 1 a s + b s s

Alias of the forward direction of convex_iff_pointwise_add_subset.

theorem convex_empty {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] :
convex 𝕜
theorem convex_univ {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] :
theorem convex.inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {s t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :
convex 𝕜 (s t)
theorem convex_sInter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {S : set (set E)} (h : (s : set E), s S convex 𝕜 s) :
convex 𝕜 (⋂₀ S)
theorem convex_Inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {ι : Sort u_3} {s : ι set E} (h : (i : ι), convex 𝕜 (s i)) :
convex 𝕜 ( (i : ι), s i)
theorem convex_Inter₂ {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {ι : Sort u_3} {κ : ι Sort u_4} {s : Π (i : ι), κ i set E} (h : (i : ι) (j : κ i), convex 𝕜 (s i j)) :
convex 𝕜 ( (i : ι) (j : κ i), s i j)
theorem convex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [has_smul 𝕜 E] [has_smul 𝕜 F] {s : set E} {t : set F} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :
convex 𝕜 (s ×ˢ t)
theorem convex_pi {𝕜 : Type u_1} [ordered_semiring 𝕜] {ι : Type u_2} {E : ι Type u_3} [Π (i : ι), add_comm_monoid (E i)] [Π (i : ι), has_smul 𝕜 (E i)] {s : set ι} {t : Π (i : ι), set (E i)} (ht : ⦃i : ι⦄, i s convex 𝕜 (t i)) :
convex 𝕜 (s.pi t)
theorem directed.convex_Union {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {ι : Sort u_3} {s : ι set E} (hdir : directed has_subset.subset s) (hc : ⦃i : ι⦄, convex 𝕜 (s i)) :
convex 𝕜 ( (i : ι), s i)
theorem directed_on.convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {c : set (set E)} (hdir : directed_on has_subset.subset c) (hc : ⦃A : set E⦄, A c convex 𝕜 A) :
convex 𝕜 (⋃₀ c)
theorem convex_iff_open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :
convex 𝕜 s ⦃x : E⦄, x s ⦃y : E⦄, y s open_segment 𝕜 x y s
theorem convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :
convex 𝕜 s ⦃x : E⦄, x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a x + b y s
theorem convex_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :
convex 𝕜 s s.pairwise (λ (x y : E), ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a x + b y s)
theorem convex.star_convex_iff {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} {x : E} (hs : convex 𝕜 s) (h : s.nonempty) :
star_convex 𝕜 x s x s
@[protected]
theorem set.subsingleton.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (h : s.subsingleton) :
convex 𝕜 s
theorem convex_singleton {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (c : E) :
convex 𝕜 {c}
theorem convex_zero {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] :
convex 𝕜 0
theorem convex_segment {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (x y : E) :
convex 𝕜 (segment 𝕜 x y)
theorem convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set E} (hs : convex 𝕜 s) (f : E →ₗ[𝕜] F) :
convex 𝕜 (f '' s)
theorem convex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set E} (hs : convex 𝕜 s) {f : E F} (hf : is_linear_map 𝕜 f) :
convex 𝕜 (f '' s)
theorem convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : convex 𝕜 s) (f : E →ₗ[𝕜] F) :
convex 𝕜 (f ⁻¹' s)
theorem convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : convex 𝕜 s) {f : E F} (hf : is_linear_map 𝕜 f) :
convex 𝕜 (f ⁻¹' s)
theorem convex.add {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :
convex 𝕜 (s + t)
def convex_add_submonoid (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] :

The convex sets form an additive submonoid under pointwise addition.

Equations
@[simp, norm_cast]
theorem coe_convex_add_submonoid (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] :
(convex_add_submonoid 𝕜 E) = {s : set E | convex 𝕜 s}
@[simp]
theorem mem_convex_add_submonoid {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :
theorem convex_list_sum {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {l : list (set E)} (h : (i : set E), i l convex 𝕜 i) :
convex 𝕜 l.sum
theorem convex_multiset_sum {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : multiset (set E)} (h : (i : set E), i s convex 𝕜 i) :
convex 𝕜 s.sum
theorem convex_sum {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {ι : Type u_3} {s : finset ι} (t : ι set E) (h : (i : ι), i s convex 𝕜 (t i)) :
convex 𝕜 (s.sum (λ (i : ι), t i))
theorem convex.vadd {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (z : E) :
convex 𝕜 (z +ᵥ s)
theorem convex.translate {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (z : E) :
convex 𝕜 ((λ (x : E), z + x) '' s)
theorem convex.translate_preimage_right {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (z : E) :
convex 𝕜 ((λ (x : E), z + x) ⁻¹' s)

The translation of a convex set is also convex.

theorem convex.translate_preimage_left {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (z : E) :
convex 𝕜 ((λ (x : E), x + z) ⁻¹' s)

The translation of a convex set is also convex.

theorem convex_Iic {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :
convex 𝕜 (set.Iic r)
theorem convex_Ici {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :
convex 𝕜 (set.Ici r)
theorem convex_Icc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :
convex 𝕜 (set.Icc r s)
theorem convex_halfspace_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} (h : is_linear_map 𝕜 f) (r : β) :
convex 𝕜 {w : E | f w r}
theorem convex_halfspace_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} (h : is_linear_map 𝕜 f) (r : β) :
convex 𝕜 {w : E | r f w}
theorem convex_hyperplane {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} (h : is_linear_map 𝕜 f) (r : β) :
convex 𝕜 {w : E | f w = r}
theorem convex_Iio {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :
convex 𝕜 (set.Iio r)
theorem convex_Ioi {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :
convex 𝕜 (set.Ioi r)
theorem convex_Ioo {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :
convex 𝕜 (set.Ioo r s)
theorem convex_Ico {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :
convex 𝕜 (set.Ico r s)
theorem convex_Ioc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :
convex 𝕜 (set.Ioc r s)
theorem convex_halfspace_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} (h : is_linear_map 𝕜 f) (r : β) :
convex 𝕜 {w : E | f w < r}
theorem convex_halfspace_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} (h : is_linear_map 𝕜 f) (r : β) :
convex 𝕜 {w : E | r < f w}
theorem convex_uIcc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :
convex 𝕜 (set.uIcc r s)
theorem monotone_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | f x r}
theorem monotone_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | f x < r}
theorem monotone_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | r f x}
theorem monotone_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | r < f x}
theorem antitone_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | f x r}
theorem antitone_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | f x < r}
theorem antitone_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | r f x}
theorem antitone_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :
convex 𝕜 {x ∈ s | r < f x}
theorem monotone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : monotone f) (r : β) :
convex 𝕜 {x : E | f x r}
theorem monotone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : monotone f) (r : β) :
convex 𝕜 {x : E | f x r}
theorem monotone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : monotone f) (r : β) :
convex 𝕜 {x : E | r f x}
theorem monotone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : monotone f) (r : β) :
convex 𝕜 {x : E | f x r}
theorem antitone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : antitone f) (r : β) :
convex 𝕜 {x : E | f x r}
theorem antitone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : antitone f) (r : β) :
convex 𝕜 {x : E | f x < r}
theorem antitone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : antitone f) (r : β) :
convex 𝕜 {x : E | r f x}
theorem antitone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E β} (hf : antitone f) (r : β) :
convex 𝕜 {x : E | r < f x}
theorem convex.smul {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (c : 𝕜) :
convex 𝕜 (c s)
theorem convex.smul_preimage {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (c : 𝕜) :
convex 𝕜 ((λ (z : E), c z) ⁻¹' s)
theorem convex.affinity {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (z : E) (c : 𝕜) :
convex 𝕜 ((λ (x : E), z + c x) '' s)
theorem convex_open_segment {𝕜 : Type u_1} {E : Type u_2} [strict_ordered_comm_semiring 𝕜] [add_comm_group E] [module 𝕜 E] (a b : E) :
convex 𝕜 (open_segment 𝕜 a b)
theorem convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x s) (hy : x + y s) {t : 𝕜} (ht : t set.Icc 0 1) :
x + t y s
theorem convex.smul_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x : E} (zero_mem : 0 s) (hx : x s) {t : 𝕜} (ht : t set.Icc 0 1) :
t x s
theorem convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (h : convex 𝕜 s) {x y : E} (hx : x s) (hy : y s) {t : 𝕜} (ht : t set.Icc 0 1) :
x + t (y - x) s
theorem affine_subspace.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (Q : affine_subspace 𝕜 E) :
convex 𝕜 Q

Affine subspaces are convex.

theorem convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : set F} (hs : convex 𝕜 s) :
convex 𝕜 (f ⁻¹' s)

The preimage of a convex set under an affine map is convex.

theorem convex.affine_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E} (f : E →ᵃ[𝕜] F) (hs : convex 𝕜 s) :
convex 𝕜 (f '' s)

The image of a convex set under an affine map is convex.

theorem convex.neg {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) :
convex 𝕜 (-s)
theorem convex.sub {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :
convex 𝕜 (s - t)
theorem convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} :
convex 𝕜 s ⦃x : E⦄, x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 a 0 b 0 < a + b (a / (a + b)) x + (b / (a + b)) y s

Alternative definition of set convexity, using division.

theorem convex.mem_smul_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (h : convex 𝕜 s) {x : E} (zero_mem : 0 s) (hx : x s) {t : 𝕜} (ht : 1 t) :
x t s
theorem convex.add_smul {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (h_conv : convex 𝕜 s) {p q : 𝕜} (hp : 0 p) (hq : 0 q) :
(p + q) s = p s + q s

Convex sets in an ordered space #

Relates convex and ord_connected.

theorem set.ord_connected.convex_of_chain {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : is_chain has_le.le s) :
convex 𝕜 s
theorem set.ord_connected.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :
convex 𝕜 s
theorem convex_iff_ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] {s : set 𝕜} :
theorem convex.ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] {s : set 𝕜} :

Alias of the forward direction of convex_iff_ord_connected.

Convexity of submodules/subspaces #

@[protected]
theorem submodule.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (K : submodule 𝕜 E) :
convex 𝕜 K
@[protected]
theorem submodule.star_convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (K : submodule 𝕜 E) :

Simplex #

def std_simplex (𝕜 : Type u_1) (ι : Type u_5) [ordered_semiring 𝕜] [fintype ι] :
set 𝕜)

The standard simplex in the space of functions ι → 𝕜 is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

Equations
theorem std_simplex_eq_inter (𝕜 : Type u_1) (ι : Type u_5) [ordered_semiring 𝕜] [fintype ι] :
std_simplex 𝕜 ι = ( (x : ι), {f : ι 𝕜 | 0 f x}) {f : ι 𝕜 | finset.univ.sum (λ (x : ι), f x) = 1}
theorem convex_std_simplex (𝕜 : Type u_1) (ι : Type u_5) [ordered_semiring 𝕜] [fintype ι] :
convex 𝕜 (std_simplex 𝕜 ι)
theorem ite_eq_mem_std_simplex (𝕜 : Type u_1) {ι : Type u_5} [ordered_semiring 𝕜] [fintype ι] (i : ι) :
(λ (j : ι), ite (i = j) 1 0) std_simplex 𝕜 ι