# mathlibdocumentation

analysis.convex.basic

# 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.
• std_simplex π ΞΉ: 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} [ordered_semiring π] [has_smul π E] (s : set E) :
Prop

Convexity of sets.

Equations
theorem convex.star_convex {π : Type u_1} {E : Type u_2} [ordered_semiring π] [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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [has_smul π E] :
convex π β
theorem convex_univ {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] :
convex π set.univ
theorem convex.inter {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {s t : set E} (hs : convex π s) (ht : convex π t) :
theorem convex_sInter {π : Type u_1} {E : Type u_2} [ordered_semiring π] [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 π] [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 π] [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 π] [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 π] [has_smul π E] {ΞΉ : Sort u_3} {s : ΞΉ β set E} (hdir : s) (hc : β β¦i : ΞΉβ¦, convex π (s i)) :
convex π (β (i : ΞΉ), s i)
theorem directed_on.convex_sUnion {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_smul π E] {c : set (set E)} (hdir : 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 π] [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 π] [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 π] [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 π] [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 π] [module π E] {s : set E} (h : s.subsingleton) :
convex π s
theorem convex_singleton {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (c : E) :
convex π {c}
theorem convex_segment {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (x y : E) :
convex π (segment π x y)
theorem convex_open_segment {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (a b : E) :
convex π (open_segment π a b)
theorem convex.linear_image {π : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π] [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 π] [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 π] [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 π] [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 π] [module π E] {s t : set E} (hs : convex π s) (ht : convex π t) :
convex π (s + t)
theorem convex.vadd {π : Type u_1} {E : Type u_2} [ordered_semiring π] [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 π] [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 π] [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 π] [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 π] [module π Ξ²] [ordered_smul π Ξ²] (r : Ξ²) :
convex π (set.Iic r)
theorem convex_Ici {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [module π Ξ²] [ordered_smul π Ξ²] (r : Ξ²) :
convex π (set.Ici r)
theorem convex_Icc {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [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 π] [module π E] [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 π] [module π E] [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 π] [module π E] [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 π] [module π Ξ²] [ordered_smul π Ξ²] (r : Ξ²) :
convex π (set.Iio r)
theorem convex_Ioi {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [module π Ξ²] [ordered_smul π Ξ²] (r : Ξ²) :
convex π (set.Ioi r)
theorem convex_Ioo {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [module π Ξ²] [ordered_smul π Ξ²] (r s : Ξ²) :
convex π (set.Ioo r s)
theorem convex_Ico {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [module π Ξ²] [ordered_smul π Ξ²] (r s : Ξ²) :
convex π (set.Ico r s)
theorem convex_Ioc {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [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 π] [module π E] [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 π] [module π E] [module π Ξ²] [ordered_smul π Ξ²] {f : E β Ξ²} (h : is_linear_map π f) (r : Ξ²) :
convex π {w : E | r < f w}
theorem convex_interval {π : Type u_1} {Ξ² : Type u_4} [ordered_semiring π] [module π Ξ²] [ordered_smul π Ξ²] (r s : Ξ²) :
convex π s)
theorem monotone_on.convex_le {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [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 π] [module π E] {s : set E} (hs : convex π s) (z : E) (c : π) :
convex π ((Ξ» (x : E), z + c β’ x) '' s)
theorem convex.add_smul_mem {π : Type u_1} {E : Type u_2} [ordered_ring π] [module π E] {s : set E} (hs : convex π s) {x y : E} (hx : x β s) (hy : x + y β s) {t : π} (ht : t β 1) :
x + t β’ y β s
theorem convex.smul_mem_of_zero_mem {π : Type u_1} {E : Type u_2} [ordered_ring π] [module π E] {s : set E} (hs : convex π s) {x : E} (zero_mem : 0 β s) (hx : x β s) {t : π} (ht : t β 1) :
theorem convex.add_smul_sub_mem {π : Type u_1} {E : Type u_2} [ordered_ring π] [module π E] {s : set E} (h : convex π s) {x y : E} (hx : x β s) (hy : y β s) {t : π} (ht : t β 1) :
x + t β’ (y - x) β s
theorem affine_subspace.convex {π : Type u_1} {E : Type u_2} [ordered_ring π] [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 π] [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 π] [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 π] [module π E] {s : set E} (hs : convex π s) :
convex π (-s)
theorem convex.sub {π : Type u_1} {E : Type u_2} [ordered_ring π] [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 π] [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 π] [module π E] {s : set E} (h : convex π s) {x : E} (zero_mem : 0 β s) (hx : x β s) {t : π} (ht : 1 β€ t) :
theorem convex.add_smul {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [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 π] [module π E] [ordered_smul π E] {s : set E} (hs : s.ord_connected) (h : s) :
convex π s
theorem set.ord_connected.convex {π : Type u_1} {E : Type u_2} [ordered_semiring π] [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 π} :
convex π s β s.ord_connected

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 π] [module π E] (K : submodule π E) :
convex π βK
@[protected]
theorem submodule.star_convex {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (K : submodule π E) :
star_convex π 0 βK

### 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 π ΞΉ