Convex sets and functions in vector spaces

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

• Convex 𝕜 s: A set s is convex if for any two points x y ∈ s it includes segment 𝕜 x y.
• stdSimplex 𝕜 ι: The standard simplex in ι → 𝕜 (currently requires Fintype ι). It is the intersection of the positive quadrant with the hyperplane s.sum = 1.

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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) : Prop

Convexity of sets.

Equations

• Convex 𝕜 s = ∀ ⦃x : E⦄, x ∈ s → StarConvex 𝕜 x s

theorem Convex.starConvex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} (hs : Convex 𝕜 s) (hx : x ∈ s) : StarConvex 𝕜 x s

theorem convex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) : segment 𝕜 x y ⊆ s

theorem Convex.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s

theorem convex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [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} [OrderedSemiring 𝕜] [AddCommMonoid E] [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.

---

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

theorem convex_empty {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Convex 𝕜 ∅

theorem convex_univ {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Convex 𝕜 Set.univ

theorem Convex.inter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ∩ t)

theorem convex_sInter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) : Convex 𝕜 (⋂₀ S)

theorem convex_iInter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E} (h : ∀ (i : ι), Convex 𝕜 (s i)) : Convex 𝕜 (⋂ (i : ι), s i)

theorem convex_iInter₂ {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {κ : ι → Sort u_6} {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [SMul 𝕜 E] [SMul 𝕜 F] {s : Set E} {t : Set F} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ×ˢ t)

theorem convex_pi {𝕜 : Type u_1} [OrderedSemiring 𝕜] {ι : Type u_5} {E : ι → Type u_6} [(i : ι) → AddCommMonoid (E i)] [(i : ι) → SMul 𝕜 (E i)] {s : Set ι} {t : (i : ι) → Set (E i)} (ht : ∀ ⦃i : ι⦄, i ∈ s → Convex 𝕜 (t i)) : Convex 𝕜 (s.pi t)

theorem Directed.convex_iUnion {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E} (hdir : Directed (fun (x1 x2 : Set E) => x1 ⊆ x2) s) (hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)) : Convex 𝕜 (⋃ (i : ι), s i)

theorem DirectedOn.convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {c : Set (Set E)} (hdir : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) c) (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) : Convex 𝕜 (⋃₀ c)

theorem convex_iff_openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

theorem convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ s.Pairwise fun (x y : E) => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

theorem Convex.starConvex_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} (hs : Convex 𝕜 s) (h : s.Nonempty) : StarConvex 𝕜 x s ↔ x ∈ s

theorem Set.Subsingleton.convex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : s.Subsingleton) : Convex 𝕜 s

theorem convex_singleton {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (c : E) : Convex 𝕜 {c}

theorem convex_zero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Convex 𝕜 0

theorem convex_segment {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) (y : E) : Convex 𝕜 (segment 𝕜 x y)

theorem Convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) : Convex 𝕜 (f '' s)

theorem Convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) : Convex 𝕜 (f ⁻¹' s)

theorem Convex.add {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s + t)

def convexAddSubmonoid (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : AddSubmonoid (Set E)

The convex sets form an additive submonoid under pointwise addition.

Equations

• convexAddSubmonoid 𝕜 E = { carrier := {s : Set E | Convex 𝕜 s}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem coe_convexAddSubmonoid (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ↑(convexAddSubmonoid 𝕜 E) = {s : Set E | Convex 𝕜 s}

@[simp]

theorem mem_convexAddSubmonoid {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s

theorem convex_list_sum {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {l : List (Set E)} (h : ∀ i ∈ l, Convex 𝕜 i) : Convex 𝕜 l.sum

theorem convex_multiset_sum {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) : Convex 𝕜 s.sum

theorem convex_sum {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ι : Type u_5} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, Convex 𝕜 (t i)) : Convex 𝕜 (∑ i ∈ s, t i)

theorem Convex.vadd {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 (z +ᵥ s)

theorem Convex.translate {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun (x : E) => z + x) '' s)

theorem Convex.translate_preimage_right {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun (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} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun (x : E) => x + z) ⁻¹' s)

The translation of a convex set is also convex.

theorem convex_Iic {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : Convex 𝕜 (Set.Iic r)

theorem convex_Ici {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : Convex 𝕜 (Set.Ici r)

theorem convex_Icc {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) (s : β) : Convex 𝕜 (Set.Icc r s)

theorem convex_halfspace_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [OrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | f w ≤ r}

theorem convex_halfspace_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [OrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | r ≤ f w}

theorem convex_hyperplane {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [OrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | f w = r}

theorem convex_Iio {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : Convex 𝕜 (Set.Iio r)

theorem convex_Ioi {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : Convex 𝕜 (Set.Ioi r)

theorem convex_Ioo {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) (s : β) : Convex 𝕜 (Set.Ioo r s)

theorem convex_Ico {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) (s : β) : Convex 𝕜 (Set.Ico r s)

theorem convex_Ioc {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) (s : β) : Convex 𝕜 (Set.Ioc r s)

theorem convex_halfspace_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | f w < r}

theorem convex_halfspace_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [OrderedCancelAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | r < f w}

theorem convex_uIcc {𝕜 : Type u_1} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) (s : β) : Convex 𝕜 (Set.uIcc r s)

theorem MonotoneOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}

theorem MonotoneOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

theorem MonotoneOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}

theorem MonotoneOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

theorem AntitoneOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}

theorem AntitoneOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

theorem AntitoneOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}

theorem AntitoneOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

theorem Monotone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 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} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) : Convex 𝕜 {x : E | r < f x}

theorem Convex.smul {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 (c • s)

theorem Convex.smul_preimage {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 ((fun (z : E) => c • z) ⁻¹' s)

theorem Convex.affinity {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) (c : 𝕜) : Convex 𝕜 ((fun (x : E) => z + c • x) '' s)

theorem convex_openSegment {𝕜 : Type u_1} {E : Type u_2} [StrictOrderedCommSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) : Convex 𝕜 (openSegment 𝕜 a b)

@[simp]

theorem convex_vadd {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (a : E) : Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s

theorem Convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {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} [OrderedRing 𝕜] [AddCommGroup 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.mapsTo_lineMap {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) : Set.MapsTo (⇑(AffineMap.lineMap x y)) (Set.Icc 0 1) s

theorem Convex.lineMap_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : (AffineMap.lineMap x y) t ∈ s

theorem Convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : x + t • (y - x) ∈ s

theorem AffineSubspace.convex {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (Q : AffineSubspace 𝕜 E) : Convex 𝕜 ↑Q

Affine subspaces are convex.

theorem Convex.affine_preimage {𝕜 : 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 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} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup 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} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (-s)

theorem Convex.sub {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s - t)

theorem Convex_subadditive_le {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y) (hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) : Convex 𝕜 {x : E | f x ≤ B}

theorem convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup 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} [LinearOrderedField 𝕜] [AddCommGroup 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.exists_mem_add_smul_eq {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} {y : E} {p : 𝕜} {q : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (hp : 0 ≤ p) (hq : 0 ≤ q) : ∃ z ∈ s, (p + q) • z = p • x + q • y

theorem Convex.add_smul {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup 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 OrdConnected.

theorem Set.OrdConnected.convex_of_chain {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (fun (x1 x2 : E) => x1 ≤ x2) s) : Convex 𝕜 s

theorem Set.OrdConnected.convex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} (hs : s.OrdConnected) : Convex 𝕜 s

theorem convex_iff_ordConnected {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} : Convex 𝕜 s ↔ s.OrdConnected

theorem Convex.ordConnected {𝕜 : Type u_1} [LinearOrderedField 𝕜] {s : Set 𝕜} : Convex 𝕜 s → s.OrdConnected

Alias of the forward direction of convex_iff_ordConnected.

Convexity of submodules/subspaces

theorem Submodule.convex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (K : Submodule 𝕜 E) : Convex 𝕜 ↑K

theorem Submodule.starConvex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (K : Submodule 𝕜 E) : StarConvex 𝕜 0 ↑K

Simplex

def stdSimplex (𝕜 : Type u_1) (ι : Type u_5) [OrderedSemiring 𝕜] [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

• stdSimplex 𝕜 ι = {f : ι → 𝕜 | (∀ (x : ι), 0 ≤ f x) ∧ ∑ x : ι, f x = 1}

theorem stdSimplex_eq_inter (𝕜 : Type u_1) (ι : Type u_5) [OrderedSemiring 𝕜] [Fintype ι] : stdSimplex 𝕜 ι = (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | ∑ x : ι, f x = 1}

theorem convex_stdSimplex (𝕜 : Type u_1) (ι : Type u_5) [OrderedSemiring 𝕜] [Fintype ι] : Convex 𝕜 (stdSimplex 𝕜 ι)

theorem stdSimplex_of_subsingleton (𝕜 : Type u_1) (ι : Type u_5) [OrderedSemiring 𝕜] [Fintype ι] [Subsingleton 𝕜] : stdSimplex 𝕜 ι = Set.univ

theorem stdSimplex_of_isEmpty_index (𝕜 : Type u_1) (ι : Type u_5) [OrderedSemiring 𝕜] [Fintype ι] [IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅

The standard simplex in the zero-dimensional space is empty.

theorem stdSimplex_unique (𝕜 : Type u_1) (ι : Type u_5) [OrderedSemiring 𝕜] [Fintype ι] [Nonempty ι] [Subsingleton ι] : stdSimplex 𝕜 ι = {fun (x : ι) => 1}

theorem single_mem_stdSimplex (𝕜 : Type u_1) {ι : Type u_5} [OrderedSemiring 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) : Pi.single i 1 ∈ stdSimplex 𝕜 ι

theorem ite_eq_mem_stdSimplex (𝕜 : Type u_1) {ι : Type u_5} [OrderedSemiring 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) : (fun (x : ι) => if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι

theorem segment_single_subset_stdSimplex (𝕜 : Type u_1) {ι : Type u_5} [OrderedSemiring 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) (j : ι) : segment 𝕜 (Pi.single i 1) (Pi.single j 1) ⊆ stdSimplex 𝕜 ι

The edges are contained in the simplex.

theorem stdSimplex_fin_two (𝕜 : Type u_1) [OrderedSemiring 𝕜] : stdSimplex 𝕜 (Fin 2) = segment 𝕜 (Pi.single 0 1) (Pi.single 1 1)

def stdSimplexEquivIcc (𝕜 : Type u_1) [OrderedRing 𝕜] : ↑(stdSimplex 𝕜 (Fin 2)) ≃ ↑(Set.Icc 0 1)

The standard one-dimensional simplex in Fin 2 → 𝕜 is equivalent to the unit interval.

Equations

• stdSimplexEquivIcc 𝕜 = { toFun := fun (f : ↑(stdSimplex 𝕜 (Fin 2))) => ⟨↑f 0, ⋯⟩, invFun := fun (x : ↑(Set.Icc 0 1)) => ⟨![↑x, 1 - ↑x], ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem stdSimplexEquivIcc_apply_coe (𝕜 : Type u_1) [OrderedRing 𝕜] (f : ↑(stdSimplex 𝕜 (Fin 2))) : ↑((stdSimplexEquivIcc 𝕜) f) = ↑f 0

@[simp]

theorem stdSimplexEquivIcc_symm_apply_coe (𝕜 : Type u_1) [OrderedRing 𝕜] (x : ↑(Set.Icc 0 1)) : ↑((stdSimplexEquivIcc 𝕜).symm x) = ![↑x, 1 - ↑x]