# mathlib3documentation

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.

• 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} [ E] (s : set E) :
Prop

Convexity of sets.

Equations
theorem convex.star_convex {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {x : E} (hs : s) (hx : x s) :
x s
theorem convex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
s ⦃x : E⦄, x s ⦃y : E⦄, y s x y s
theorem convex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (h : s) {x y : E} (hx : x s) (hy : y s) :
x y s
theorem convex.open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (h : s) {x y : E} (hx : x s) (hy : y s) :
x y s
theorem convex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
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} [ E] {s : set E} :
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} [ E] :
theorem convex_univ {𝕜 : Type u_1} {E : Type u_2} [ E] :
theorem convex.inter {𝕜 : Type u_1} {E : Type u_2} [ E] {s t : set E} (hs : s) (ht : t) :
(s t)
theorem convex_sInter {𝕜 : Type u_1} {E : Type u_2} [ E] {S : set (set E)} (h : (s : set E), s S s) :
(⋂₀ S)
theorem convex_Inter {𝕜 : Type u_1} {E : Type u_2} [ E] {ι : Sort u_3} {s : ι set E} (h : (i : ι), (s i)) :
( (i : ι), s i)
theorem convex_Inter₂ {𝕜 : Type u_1} {E : Type u_2} [ E] {ι : Sort u_3} {κ : ι Sort u_4} {s : Π (i : ι), κ i set E} (h : (i : ι) (j : κ i), (s i j)) :
( (i : ι) (j : κ i), s i j)
theorem convex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {s : set E} {t : set F} (hs : s) (ht : t) :
(s ×ˢ t)
theorem convex_pi {𝕜 : Type u_1} {ι : Type u_2} {E : ι Type u_3} [Π (i : ι), add_comm_monoid (E i)] [Π (i : ι), (E i)] {s : set ι} {t : Π (i : ι), set (E i)} (ht : ⦃i : ι⦄, i s (t i)) :
(s.pi t)
theorem directed.convex_Union {𝕜 : Type u_1} {E : Type u_2} [ E] {ι : Sort u_3} {s : ι set E} (hdir : s) (hc : ⦃i : ι⦄, (s i)) :
( (i : ι), s i)
theorem directed_on.convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [ E] {c : set (set E)} (hdir : c) (hc : ⦃A : set E⦄, A c A) :
(⋃₀ c)
theorem convex_iff_open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
s ⦃x : E⦄, x s ⦃y : E⦄, y s x y s
theorem convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
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} [ E] {s : set E} :
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} [ E] {s : set E} {x : E} (hs : s) (h : s.nonempty) :
x s x s
@[protected]
theorem set.subsingleton.convex {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (h : s.subsingleton) :
s
theorem convex_singleton {𝕜 : Type u_1} {E : Type u_2} [ E] (c : E) :
{c}
theorem convex_zero {𝕜 : Type u_1} {E : Type u_2} [ E] :
0
theorem convex_segment {𝕜 : Type u_1} {E : Type u_2} [ E] (x y : E) :
(segment 𝕜 x y)
theorem convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {s : set E} (hs : s) (f : E →ₗ[𝕜] F) :
(f '' s)
theorem convex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {s : set E} (hs : s) {f : E F} (hf : f) :
(f '' s)
theorem convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {s : set F} (hs : s) (f : E →ₗ[𝕜] F) :
(f ⁻¹' s)
theorem convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {s : set F} (hs : s) {f : E F} (hf : f) :
(f ⁻¹' s)
theorem convex.add {𝕜 : Type u_1} {E : Type u_2} [ E] {s t : set E} (hs : s) (ht : t) :
(s + t)
def convex_add_submonoid (𝕜 : Type u_1) (E : Type u_2) [ E] :

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

The translation of a convex set is also convex.

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

Affine subspaces are convex.

theorem convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [ E] [ F] (f : E →ᵃ[𝕜] F) {s : set F} (hs : s) :
(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 𝕜] [ E] [ F] {s : set E} (f : E →ᵃ[𝕜] F) (hs : s) :
(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 𝕜] [ E] {s : set E} (hs : s) :
(-s)
theorem convex.sub {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [ E] {s t : set E} (hs : s) (ht : t) :
(s - t)
theorem convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
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} [ E] {s : set E} (h : 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} [ E] {s : set E} (h_conv : 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} [ E] [ E] {s : set E} (hs : s.ord_connected) (h : s) :
s
theorem set.ord_connected.convex {𝕜 : Type u_1} {E : Type u_2} [ E] [ E] {s : set E} (hs : s.ord_connected) :
s
theorem convex_iff_ord_connected {𝕜 : Type u_1} {s : set 𝕜} :
theorem convex.ord_connected {𝕜 : Type u_1} {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} [ E] (K : E) :
K
@[protected]
theorem submodule.star_convex {𝕜 : Type u_1} {E : Type u_2} [ E] (K : E) :
0 K

### Simplex #

def std_simplex (𝕜 : Type u_1) (ι : Type u_5) [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) [fintype ι] :
ι = ( (x : ι), {f : ι 𝕜 | 0 f x}) {f : ι 𝕜 | finset.univ.sum (λ (x : ι), f x) = 1}
theorem convex_std_simplex (𝕜 : Type u_1) (ι : Type u_5) [fintype ι] :
ι)
theorem ite_eq_mem_std_simplex (𝕜 : Type u_1) {ι : Type u_5} [fintype ι] (i : ι) :
(λ (j : ι), ite (i = j) 1 0) ι