# 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 π] [] [SMul π E] (s : Set E) :

Convexity of sets.

Equations
Instances For
theorem Convex.starConvex {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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 π] [] [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 π] [] [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 π] [] [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 π] [] [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 π] [] [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 π] [] [SMul π E] :
Convex π β
theorem convex_univ {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [SMul π E] :
Convex π Set.univ
theorem Convex.inter {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [SMul π E] {s : Set E} {t : Set E} (hs : Convex π s) (ht : Convex π t) :
theorem convex_sInter {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [SMul π E] {S : Set (Set E)} (h : β s β S, Convex π s) :
Convex π ()
theorem convex_iInter {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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 π] [] [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 π] [] [] [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 π] [] [SMul π E] {ΞΉ : Sort u_5} {s : ΞΉ β Set E} (hdir : Directed (fun (x x_1 : Set E) => x β x_1) s) (hc : β β¦i : ΞΉβ¦, Convex π (s i)) :
Convex π (β (i : ΞΉ), s i)
theorem DirectedOn.convex_sUnion {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [SMul π E] {c : Set (Set E)} (hdir : DirectedOn (fun (x x_1 : Set E) => x β x_1) c) (hc : β β¦A : Set Eβ¦, A β c β Convex π A) :
Convex π ()
theorem convex_iff_openSegment_subset {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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 π] [] [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 π] [] [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 π] [] [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 π] [] [Module π E] {s : Set E} (h : s.Subsingleton) :
Convex π s
theorem convex_singleton {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [Module π E] (c : E) :
Convex π {c}
theorem convex_zero {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [Module π E] :
Convex π 0
theorem convex_segment {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [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 π] [] [Module π E] :

Equations
Instances For
@[simp]
theorem coe_convexAddSubmonoid (π : Type u_1) (E : Type u_2) [OrderedSemiring π] [] [Module π E] :
β(convexAddSubmonoid π E) = {s : Set E | Convex π s}
@[simp]
theorem mem_convexAddSubmonoid {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [Module π E] {s : Set E} :
s β convexAddSubmonoid π E β Convex π s
theorem convex_list_sum {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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 π] [] [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 π] [] [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 π] [] [Module π E] {s : Set E} (hs : Convex π s) (z : E) :
Convex π (z +α΅₯ s)
theorem Convex.translate {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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 π] [] [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 π] [] [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 π] [] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) :
Convex π ()
theorem convex_Ici {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) :
Convex π ()
theorem convex_Icc {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) (s : Ξ²) :
Convex π (Set.Icc r s)
theorem convex_halfspace_le {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [] [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 π] [] [Module π E] [] [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 π] [] [Module π E] [] [Module π Ξ²] [OrderedSMul π Ξ²] {f : E β Ξ²} (h : IsLinearMap π f) (r : Ξ²) :
Convex π {w : E | f w = r}
theorem convex_Iio {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) :
Convex π ()
theorem convex_Ioi {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) :
Convex π ()
theorem convex_Ioo {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) (s : Ξ²) :
Convex π (Set.Ioo r s)
theorem convex_Ico {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) (s : Ξ²) :
Convex π (Set.Ico r s)
theorem convex_Ioc {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) (s : Ξ²) :
Convex π (Set.Ioc r s)
theorem convex_halfspace_lt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [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 π] [] [Module π E] [Module π Ξ²] [OrderedSMul π Ξ²] {f : E β Ξ²} (h : IsLinearMap π f) (r : Ξ²) :
Convex π {w : E | r < f w}
theorem convex_uIcc {π : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π] [Module π Ξ²] [OrderedSMul π Ξ²] (r : Ξ²) (s : Ξ²) :
Convex π (Set.uIcc r s)
theorem MonotoneOn.convex_le {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {s : Set E} {f : E β Ξ²} (hf : ) (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 π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | f x β€ r}
theorem Monotone.convex_lt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | f x β€ r}
theorem Monotone.convex_ge {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | r β€ f x}
theorem Monotone.convex_gt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | f x β€ r}
theorem Antitone.convex_le {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | f x β€ r}
theorem Antitone.convex_lt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | f x < r}
theorem Antitone.convex_ge {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | r β€ f x}
theorem Antitone.convex_gt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π] [] [Module π E] [OrderedSMul π E] {f : E β Ξ²} (hf : ) (r : Ξ²) :
Convex π {x : E | r < f x}
theorem Convex.smul {π : Type u_1} {E : Type u_2} [] [] [Module π E] {s : Set E} (hs : Convex π s) (c : π) :
Convex π (c β’ s)
theorem Convex.smul_preimage {π : Type u_1} {E : Type u_2} [] [] [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} [] [] [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} [] [] [Module π E] (a : E) (b : E) :
Convex π (openSegment π a b)
@[simp]
theorem convex_vadd {π : Type u_1} {E : Type u_2} [OrderedRing π] [] [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 π] [] [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 π] [] [Module π E] {s : Set E} (hs : Convex π s) {x : E} (zero_mem : 0 β s) (hx : x β s) {t : π} (ht : t β Set.Icc 0 1) :
theorem Convex.mapsTo_lineMap {π : Type u_1} {E : Type u_2} [OrderedRing π] [] [Module π E] {s : Set E} (h : Convex π s) {x : E} {y : E} (hx : x β s) (hy : y β s) :
Set.MapsTo (β()) (Set.Icc 0 1) s
theorem Convex.lineMap_mem {π : Type u_1} {E : Type u_2} [OrderedRing π] [] [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) :
() t β s
theorem Convex.add_smul_sub_mem {π : Type u_1} {E : Type u_2} [OrderedRing π] [] [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 π] [] [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 π] [] [] [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 π] [] [] [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 π] [] [Module π E] {s : Set E} (hs : Convex π s) :
Convex π (-s)
theorem Convex.sub {π : Type u_1} {E : Type u_2} [OrderedRing π] [] [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} [] [] [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} [] [] [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} [] [] [Module π E] {s : Set E} (h : Convex π s) {x : E} (zero_mem : 0 β s) (hx : x β s) {t : π} (ht : 1 β€ t) :
theorem Convex.exists_mem_add_smul_eq {π : Type u_1} {E : Type u_2} [] [] [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} [] [] [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 π] [Module π E] [OrderedSMul π E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (fun (x x_1 : E) => x β€ x_1) s) :
Convex π s
theorem Set.OrdConnected.convex {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [Module π E] [OrderedSMul π E] {s : Set E} (hs : s.OrdConnected) :
Convex π s
theorem convex_iff_ordConnected {π : Type u_1} [] {s : Set π} :
Convex π s β s.OrdConnected
theorem Convex.ordConnected {π : Type u_1} [] {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 π] [] [Module π E] (K : Submodule π E) :
Convex π βK
theorem Submodule.starConvex {π : Type u_1} {E : Type u_2} [OrderedSemiring π] [] [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
Instances For
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 ΞΉ] [Unique ΞΉ] :
stdSimplex π ΞΉ = {fun (x : ΞΉ) => 1}
theorem single_mem_stdSimplex (π : Type u_1) {ΞΉ : Type u_5} [OrderedSemiring π] [Fintype ΞΉ] [] (i : ΞΉ) :
β stdSimplex π ΞΉ
theorem ite_eq_mem_stdSimplex (π : Type u_1) {ΞΉ : Type u_5} [OrderedSemiring π] [Fintype ΞΉ] [] (i : ΞΉ) :
(fun (x : ΞΉ) => if i = x then 1 else 0) β stdSimplex π ΞΉ
theorem segment_single_subset_stdSimplex (π : Type u_1) {ΞΉ : Type u_5} [OrderedSemiring π] [Fintype ΞΉ] [] (i : ΞΉ) (j : ΞΉ) :
segment π () () β stdSimplex π ΞΉ

The edges are contained in the simplex.

theorem stdSimplex_fin_two (π : Type u_1) [OrderedSemiring π] :
stdSimplex π (Fin 2) = segment π () ()
@[simp]
theorem stdSimplexEquivIcc_apply_coe (π : Type u_1) [OrderedRing π] (f : β(stdSimplex π (Fin 2))) :
β(() f) = βf 0
@[simp]
theorem stdSimplexEquivIcc_symm_apply_coe (π : Type u_1) [OrderedRing π] (x : β(Set.Icc 0 1)) :
β(().symm x) = ![βx, 1 - βx]
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
• = { toFun := fun (f : β(stdSimplex π (Fin 2))) => β¨βf 0, β―β©, invFun := fun (x : β(Set.Icc 0 1)) => β¨![βx, 1 - βx], β―β©, left_inv := β―, right_inv := β― }
Instances For