mathlib documentation

analysis.convex.basic

Convex sets and functions on real vector spaces

In a real 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, and prove Jensen's inequality.

Note: To define convexity for functions f : E → β, we need β to be an ordered vector space, defined using the instance ordered_semimodule ℝ β.

Notations

We use the following local notations:

They are defined using local notation, so they are not available outside of this file.

Segment

def segment {E : Type u} [add_comm_group E] [vector_space E] :
E → E → set E

Segments in a vector space

Equations
theorem segment_symm {E : Type u} [add_comm_group E] [vector_space E] (x y : E) :
segment x y = segment y x

theorem left_mem_segment {E : Type u} [add_comm_group E] [vector_space E] (x y : E) :
x segment x y

theorem right_mem_segment {E : Type u} [add_comm_group E] [vector_space E] (x y : E) :
y segment x y

theorem segment_same {E : Type u} [add_comm_group E] [vector_space E] (x : E) :
segment x x = {x}

theorem segment_eq_image {E : Type u} [add_comm_group E] [vector_space E] (x y : E) :
segment x y = (λ (θ : ), (1 - θ) x + θ y) '' set.Icc 0 1

theorem segment_eq_image' {E : Type u} [add_comm_group E] [vector_space E] (x y : E) :
segment x y = (λ (θ : ), x + θ (y - x)) '' set.Icc 0 1

theorem segment_eq_image₂ {E : Type u} [add_comm_group E] [vector_space E] (x y : E) :
segment x y = (λ (p : × ), p.fst x + p.snd y) '' {p : × | 0 p.fst 0 p.snd p.fst + p.snd = 1}

theorem segment_eq_Icc {a b : } :
a bsegment a b = set.Icc a b

theorem segment_eq_Icc' (a b : ) :
segment a b = set.Icc (min a b) (max a b)

theorem segment_eq_interval (a b : ) :

theorem mem_segment_translate {E : Type u} [add_comm_group E] [vector_space E] (a : E) {x b c : E} :
a + x segment (a + b) (a + c) x segment b c

theorem segment_translate_preimage {E : Type u} [add_comm_group E] [vector_space E] (a b c : E) :
(λ (x : E), a + x) ⁻¹' segment (a + b) (a + c) = segment b c

theorem segment_translate_image {E : Type u} [add_comm_group E] [vector_space E] (a b c : E) :
(λ (x : E), a + x) '' segment b c = segment (a + b) (a + c)

Convexity of sets

def convex {E : Type u} [add_comm_group E] [vector_space E] :
set E → Prop

Convexity of sets

Equations
theorem convex_iff_forall_pos {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : ⦄, 0 < a0 < ba + b = 1a x + b y s

theorem convex_iff_segment_subset {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex s ∀ ⦃x y : E⦄, x sy ssegment x y s

theorem convex.segment_subset {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (h : convex s) {x y : E} :
x sy ssegment x y s

theorem convex_iff_pointwise_add_subset {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex s ∀ ⦃a b : ⦄, 0 a0 ba + b = 1a s + b s s

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

theorem convex_iff_div {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : ⦄, 0 a0 b0 < a + b(a / (a + b)) x + (b / (a + b)) y s

Alternative definition of set convexity, using division

Examples of convex sets

theorem convex_empty {E : Type u} [add_comm_group E] [vector_space E] :

theorem convex_singleton {E : Type u} [add_comm_group E] [vector_space E] (c : E) :
convex {c}

theorem convex_univ {E : Type u} [add_comm_group E] [vector_space E] :

theorem convex.inter {E : Type u} [add_comm_group E] [vector_space E] {s t : set E} :
convex sconvex tconvex (s t)

theorem convex_sInter {E : Type u} [add_comm_group E] [vector_space E] {S : set (set E)} :
(∀ (s : set E), s Sconvex s)convex (⋂₀S)

theorem convex_Inter {E : Type u} [add_comm_group E] [vector_space E] {ι : Sort u_1} {s : ι → set E} :
(∀ (i : ι), convex (s i))convex (⋂ (i : ι), s i)

theorem convex.prod {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set E} {t : set F} :
convex sconvex tconvex (s.prod t)

theorem convex.combo_to_vadd {E : Type u} [add_comm_group E] [vector_space E] {a b : } {x y : E} :
a + b = 1a x + b y = b (y - x) + x

theorem convex.combo_affine_apply {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {a b : } {x y : E} {f : E →ᵃ[] F} :
a + b = 1f (a x + b y) = a f x + b f y

Applying an affine map to an affine combination of two points yields an affine combination of the images.

theorem convex.affine_preimage {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] (f : E →ᵃ[] F) {s : set F} :
convex sconvex (f ⁻¹' s)

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

theorem convex.affine_image {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] (f : E →ᵃ[] F) {s : set E} :
convex sconvex (f '' s)

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

theorem convex.linear_image {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set E} (hs : convex s) (f : E →ₗ[] F) :

theorem convex.is_linear_image {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set E} (hs : convex s) {f : E → F} :

theorem convex.linear_preimage {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set F} (hs : convex s) (f : E →ₗ[] F) :

theorem convex.is_linear_preimage {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set F} (hs : convex s) {f : E → F} :

theorem convex.neg {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex sconvex ((λ (z : E), -z) '' s)

theorem convex.neg_preimage {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex sconvex ((λ (z : E), -z) ⁻¹' s)

theorem convex.smul {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (c : ) :
convex sconvex (c s)

theorem convex.smul_preimage {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (c : ) :
convex sconvex ((λ (z : E), c z) ⁻¹' s)

theorem convex.add {E : Type u} [add_comm_group E] [vector_space E] {s t : set E} :
convex sconvex tconvex (s + t)

theorem convex.sub {E : Type u} [add_comm_group E] [vector_space E] {s t : set E} :
convex sconvex tconvex ((λ (x : E × E), x.fst - x.snd) '' s.prod t)

theorem convex.translate {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (hs : convex s) (z : E) :
convex ((λ (x : E), z + x) '' s)

theorem convex.translate_preimage_right {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (hs : convex s) (a : E) :
convex ((λ (z : E), a + z) ⁻¹' s)

The translation of a convex set is also convex

theorem convex.translate_preimage_left {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (hs : convex s) (a : E) :
convex ((λ (z : E), z + a) ⁻¹' s)

The translation of a convex set is also convex

theorem convex.affinity {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (hs : convex s) (z : E) (c : ) :
convex ((λ (x : E), z + c x) '' s)

theorem convex_Iio (r : ) :

theorem convex_Ioi (r : ) :

theorem convex_Iic (r : ) :

theorem convex_Ici (r : ) :

theorem convex_Ioo (r s : ) :

theorem convex_Ico (r s : ) :

theorem convex_Ioc (r s : ) :

theorem convex_Icc (r s : ) :

theorem convex_interval (r s : ) :

theorem convex_segment {E : Type u} [add_comm_group E] [vector_space E] (a b : E) :

theorem convex_halfspace_lt {E : Type u} [add_comm_group E] [vector_space E] {f : E → } (h : is_linear_map f) (r : ) :
convex {w : E | f w < r}

theorem convex_halfspace_le {E : Type u} [add_comm_group E] [vector_space E] {f : E → } (h : is_linear_map f) (r : ) :
convex {w : E | f w r}

theorem convex_halfspace_gt {E : Type u} [add_comm_group E] [vector_space E] {f : E → } (h : is_linear_map f) (r : ) :
convex {w : E | r < f w}

theorem convex_halfspace_ge {E : Type u} [add_comm_group E] [vector_space E] {f : E → } (h : is_linear_map f) (r : ) :
convex {w : E | r f w}

theorem convex_hyperplane {E : Type u} [add_comm_group E] [vector_space E] {f : E → } (h : is_linear_map f) (r : ) :
convex {w : E | f w = r}

theorem convex_halfspace_re_lt (r : ) :
convex {c : | c.re < r}

theorem convex_halfspace_re_le (r : ) :
convex {c : | c.re r}

theorem convex_halfspace_re_gt (r : ) :
convex {c : | r < c.re}

theorem convex_halfspace_re_lge (r : ) :
convex {c : | r c.re}

theorem convex_halfspace_im_lt (r : ) :
convex {c : | c.im < r}

theorem convex_halfspace_im_le (r : ) :
convex {c : | c.im r}

theorem convex_halfspace_im_gt (r : ) :
convex {c : | r < c.im}

theorem convex_halfspace_im_lge (r : ) :
convex {c : | r c.im}

theorem convex.combo_self {α : Type v'} [linear_ordered_field α] (a : α) {x y : α} :
x + y = 1a = x * a + y * a

theorem convex.mem_Ioo {α : Type v'} [linear_ordered_field α] {a b x : α} :
a < b(x set.Ioo a b ∃ (x_a x_b : α), 0 < x_a 0 < x_b x_a + x_b = 1 x_a * a + x_b * b = x)

If x is in an Ioo, it can be expressed as a convex combination of the endpoints.

theorem convex.mem_Ioc {α : Type v'} [linear_ordered_field α] {a b x : α} :
a < b(x set.Ioc a b ∃ (x_a x_b : α), 0 x_a 0 < x_b x_a + x_b = 1 x_a * a + x_b * b = x)

If x is in an Ioc, it can be expressed as a convex combination of the endpoints.

theorem convex.mem_Ico {α : Type v'} [linear_ordered_field α] {a b x : α} :
a < b(x set.Ico a b ∃ (x_a x_b : α), 0 < x_a 0 x_b x_a + x_b = 1 x_a * a + x_b * b = x)

If x is in an Ico, it can be expressed as a convex combination of the endpoints.

theorem convex.mem_Icc {α : Type v'} [linear_ordered_field α] {a b x : α} :
a b(x set.Icc a b ∃ (x_a x_b : α), 0 x_a 0 x_b x_a + x_b = 1 x_a * a + x_b * b = x)

If x is in an Icc, it can be expressed as a convex combination of the endpoints.

theorem submodule.convex {E : Type u} [add_comm_group E] [vector_space E] (K : submodule E) :

theorem subspace.convex {E : Type u} [add_comm_group E] [vector_space E] (K : subspace E) :

Convex functions

def convex_on {E : Type u} [add_comm_group E] [vector_space E] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] :
set E(E → β) → Prop

Convexity of functions

Equations
def concave_on {E : Type u} [add_comm_group E] [vector_space E] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] :
set E(E → β) → Prop

Concavity of functions

Equations
@[simp]
theorem neg_convex_on_iff {E : Type u} [add_comm_group E] [vector_space E] {γ : Type u_1} [ordered_add_comm_group γ] [ordered_semimodule γ] (s : set E) (f : E → γ) :

A function f is concave iff -f is convex

@[simp]
theorem neg_concave_on_iff {E : Type u} [add_comm_group E] [vector_space E] {γ : Type u_1} [ordered_add_comm_group γ] [ordered_semimodule γ] (s : set E) (f : E → γ) :

A function f is concave iff -f is convex

theorem convex_on_id {s : set } :

theorem concave_on_id {s : set } :

theorem convex_on_const {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] (c : β) :
convex sconvex_on s (λ (x : E), c)

theorem concave_on_const {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] (c : β) :
convex sconcave_on s (λ (x : E), c)

theorem convex_on_iff_div {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} :
convex_on s f convex s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : ⦄, 0 a0 b0 < a + bf ((a / (a + b)) x + (b / (a + b)) y) (a / (a + b)) f x + (b / (a + b)) f y

theorem concave_on_iff_div {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} :
concave_on s f convex s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : ⦄, 0 a0 b0 < a + b(a / (a + b)) f x + (b / (a + b)) f y f ((a / (a + b)) x + (b / (a + b)) y)

theorem linear_order.convex_on_of_lt {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} [linear_order E] :
convex s(∀ ⦃x y : E⦄, x sy sx < y∀ ⦃a b : ⦄, 0 < a0 < ba + b = 1f (a x + b y) a f x + b f y)convex_on s f

For a function on a convex set in a linear ordered space, in order to prove that it is convex it suffices to verify the inequality f (a • x + b • y) ≤ a • f x + b • f y only for x < y and positive a, b. The main use case is E = ℝ however one can apply it, e.g., to ℝ^n with lexicographic order.

theorem linear_order.concave_on_of_lt {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} [linear_order E] :
convex s(∀ ⦃x y : E⦄, x sy sx < y∀ ⦃a b : ⦄, 0 < a0 < ba + b = 1a f x + b f y f (a x + b y))concave_on s f

For a function on a convex set in a linear ordered space, in order to prove that it is concave it suffices to verify the inequality a • f x + b • f y ≤ f (a • x + b • y) only for x < y and positive a, b. The main use case is E = ℝ however one can apply it, e.g., to ℝ^n with lexicographic order.

theorem convex_on_real_of_slope_mono_adjacent {s : set } (hs : convex s) {f : } :
(∀ {x y z : }, x sz sx < yy < z(f y - f x) / (y - x) (f z - f y) / (z - y))convex_on s f

For a function f defined on a convex subset D of , if for any three points x<y<z the slope of the secant line of f on [x, y] is less than or equal to the slope of the secant line of f on [x, z], then f is convex on D. This way of proving convexity of a function is used in the proof of convexity of a function with a monotone derivative.

theorem convex_on.slope_mono_adjacent {s : set } {f : } (hf : convex_on s f) {x y z : } :
x sz sx < yy < z(f y - f x) / (y - x) (f z - f y) / (z - y)

For a function f defined on a subset D of , if f is convex on D, then for any three points x<y<z, the slope of the secant line of f on [x, y] is less than or equal to the slope of the secant line of f on [x, z].

theorem convex_on_real_iff_slope_mono_adjacent {s : set } (hs : convex s) {f : } :
convex_on s f ∀ {x y z : }, x sz sx < yy < z(f y - f x) / (y - x) (f z - f y) / (z - y)

For a function f defined on a convex subset D of , f is convex on D iff for any three points x<y<z the slope of the secant line of f on [x, y] is less than or equal to the slope of the secant line of f on [x, z].

theorem concave_on_real_of_slope_mono_adjacent {s : set } (hs : convex s) {f : } :
(∀ {x y z : }, x sz sx < yy < z(f z - f y) / (z - y) (f y - f x) / (y - x))concave_on s f

For a function f defined on a convex subset D of , if for any three points x<y<z the slope of the secant line of f on [x, y] is greater than or equal to the slope of the secant line of f on [x, z], then f is concave on D.

theorem concave_on.slope_mono_adjacent {s : set } {f : } (hf : concave_on s f) {x y z : } :
x sz sx < yy < z(f z - f y) / (z - y) (f y - f x) / (y - x)

For a function f defined on a subset D of , if f is concave on D, then for any three points x<y<z, the slope of the secant line of f on [x, y] is greater than or equal to the slope of the secant line of f on [x, z].

theorem concave_on_real_iff_slope_mono_adjacent {s : set } (hs : convex s) {f : } :
concave_on s f ∀ {x y z : }, x sz sx < yy < z(f z - f y) / (z - y) (f y - f x) / (y - x)

For a function f defined on a convex subset D of , f is concave on D iff for any three points x<y<z the slope of the secant line of f on [x, y] is greater than or equal to the slope of the secant line of f on [x, z].

theorem convex_on.subset {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {t : set E} {f : E → β} :
convex_on t fs tconvex sconvex_on s f

theorem concave_on.subset {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {t : set E} {f : E → β} :
concave_on t fs tconvex sconcave_on s f

theorem convex_on.add {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f g : E → β} :
convex_on s fconvex_on s gconvex_on s (λ (x : E), f x + g x)

theorem concave_on.add {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f g : E → β} :
concave_on s fconcave_on s gconcave_on s (λ (x : E), f x + g x)

theorem convex_on.smul {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} {c : } :
0 cconvex_on s fconvex_on s (λ (x : E), c f x)

theorem concave_on.smul {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} {c : } :
0 cconcave_on s fconcave_on s (λ (x : E), c f x)

theorem convex_on.le_on_segment' {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [linear_ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} {x y : E} {a b : } :
convex_on s fx sy s0 a0 ba + b = 1f (a x + b y) max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

theorem concave_on.le_on_segment' {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [linear_ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} {x y : E} {a b : } :
concave_on s fx sy s0 a0 ba + b = 1min (f x) (f y) f (a x + b y)

A concave function on a segment is lower-bounded by the min of its endpoints.

theorem convex_on.le_on_segment {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [linear_ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} (hf : convex_on s f) {x y z : E} :
x sy sz segment x yf z max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

theorem concave_on.le_on_segment {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [linear_ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} (hf : concave_on s f) {x y z : E} :
x sy sz segment x ymin (f x) (f y) f z

A concave function on a segment is lower-bounded by the min of its endpoints.

theorem convex_on.convex_le {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} (hf : convex_on s f) (r : β) :
convex {x ∈ s | f x r}

theorem concave_on.concave_le {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} (hf : concave_on s f) (r : β) :
convex {x ∈ s | r f x}

theorem convex_on.convex_lt {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [ordered_cancel_add_comm_monoid γ] [ordered_semimodule γ] {f : E → γ} (hf : convex_on s f) (r : γ) :
convex {x ∈ s | f x < r}

theorem concave_on.convex_lt {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [ordered_cancel_add_comm_monoid γ] [ordered_semimodule γ] {f : E → γ} (hf : concave_on s f) (r : γ) :
convex {x ∈ s | r < f x}

theorem convex_on.convex_epigraph {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} :
convex_on s fconvex {p : E × γ | p.fst s f p.fst p.snd}

theorem concave_on.convex_hypograph {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} :
concave_on s fconvex {p : E × γ | p.fst s p.snd f p.fst}

theorem convex_on_iff_convex_epigraph {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} :
convex_on s f convex {p : E × γ | p.fst s f p.fst p.snd}

theorem concave_on_iff_convex_hypograph {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [ordered_semimodule γ] {f : E → γ} :
concave_on s f convex {p : E × γ | p.fst s p.snd f p.fst}

theorem convex_on.comp_affine_map {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : F → β} (g : E →ᵃ[] F) {s : set F} :
convex_on s fconvex_on (g ⁻¹' s) (f g)

If a function is convex on s, it remains convex when precomposed by an affine map

theorem concave_on.comp_affine_map {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : F → β} (g : E →ᵃ[] F) {s : set F} :

If a function is concave on s, it remains concave when precomposed by an affine map

theorem convex_on.comp_linear_map {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {g : F → β} {s : set F} (hg : convex_on s g) (f : E →ₗ[] F) :

If g is convex on s, so is (g ∘ f) on f ⁻¹' s for a linear f.

theorem concave_on.comp_linear_map {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {g : F → β} {s : set F} (hg : concave_on s g) (f : E →ₗ[] F) :

If g is concave on s, so is (g ∘ f) on f ⁻¹' s for a linear f.

theorem convex_on.translate_right {E : Type u} [add_comm_group E] [vector_space E] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} {s : set E} {a : E} :
convex_on s fconvex_on ((λ (z : E), a + z) ⁻¹' s) (f λ (z : E), a + z)

If a function is convex on s, it remains convex after a translation.

theorem concave_on.translate_right {E : Type u} [add_comm_group E] [vector_space E] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} {s : set E} {a : E} :
concave_on s fconcave_on ((λ (z : E), a + z) ⁻¹' s) (f λ (z : E), a + z)

If a function is concave on s, it remains concave after a translation.

theorem convex_on.translate_left {E : Type u} [add_comm_group E] [vector_space E] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} {s : set E} {a : E} :
convex_on s fconvex_on ((λ (z : E), a + z) ⁻¹' s) (f λ (z : E), z + a)

If a function is convex on s, it remains convex after a translation.

theorem concave_on.translate_left {E : Type u} [add_comm_group E] [vector_space E] {β : Type u_1} [ordered_add_comm_monoid β] [ordered_semimodule β] {f : E → β} {s : set E} {a : E} :
concave_on s fconcave_on ((λ (z : E), a + z) ⁻¹' s) (f λ (z : E), z + a)

If a function is concave on s, it remains concave after a translation.

def finset.center_mass {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] :
finset ι(ι → )(ι → E) → E

Center mass of a finite collection of points with prescribed weights. Note that we require neither 0 ≤ w i nor ∑ w = 1.

Equations
theorem finset.center_mass_empty {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (w : ι → ) (z : ι → E) :

theorem finset.center_mass_pair {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (i j : ι) (w : ι → ) (z : ι → E) :
i j{i, j}.center_mass w z = (w i / (w i + w j)) z i + (w j / (w i + w j)) z j

theorem finset.center_mass_insert {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (i : ι) (t : finset ι) {w : ι → } (z : ι → E) :
i t∑ (j : ι) in t, w j 0(insert i t).center_mass w z = (w i / (w i + ∑ (j : ι) in t, w j)) z i + ((∑ (j : ι) in t, w j) / (w i + ∑ (j : ι) in t, w j)) t.center_mass w z

theorem finset.center_mass_singleton {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (i : ι) {w : ι → } (z : ι → E) :
w i 0{i}.center_mass w z = z i

theorem finset.center_mass_eq_of_sum_1 {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (t : finset ι) {w : ι → } (z : ι → E) :
∑ (i : ι) in t, w i = 1t.center_mass w z = ∑ (i : ι) in t, w i z i

theorem finset.center_mass_smul {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (c : ) (t : finset ι) {w : ι → } (z : ι → E) :
t.center_mass w (λ (i : ι), c z i) = c t.center_mass w z

theorem finset.center_mass_segment' {E : Type u} {ι : Type w} {ι' : Type x} [add_comm_group E] [vector_space E] (s : finset ι) (t : finset ι') (ws : ι → ) (zs : ι → E) (wt : ι' → ) (zt : ι' → E) (hws : ∑ (i : ι) in s, ws i = 1) (hwt : ∑ (i : ι') in t, wt i = 1) (a b : ) :
a + b = 1a s.center_mass ws zs + b t.center_mass wt zt = (finset.image sum.inl s finset.image sum.inr t).center_mass (sum.elim (λ (i : ι), a * ws i) (λ (j : ι'), b * wt j)) (sum.elim zs zt)

A convex combination of two centers of mass is a center of mass as well. This version deals with two different index types.

theorem finset.center_mass_segment {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (s : finset ι) (w₁ w₂ : ι → ) (z : ι → E) (hw₁ : ∑ (i : ι) in s, w₁ i = 1) (hw₂ : ∑ (i : ι) in s, w₂ i = 1) (a b : ) :
a + b = 1a s.center_mass w₁ z + b s.center_mass w₂ z = s.center_mass (λ (i : ι), a * w₁ i + b * w₂ i) z

A convex combination of two centers of mass is a center of mass as well. This version works if two centers of mass share the set of original points.

theorem finset.center_mass_ite_eq {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] (i : ι) (t : finset ι) (z : ι → E) :
i tt.center_mass (λ (j : ι), ite (i = j) 1 0) z = z i

theorem finset.center_mass_subset {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {t : finset ι} {w : ι → } (z : ι → E) {t' : finset ι} :
t t'(∀ (i : ι), i t'i tw i = 0)t.center_mass w z = t'.center_mass w z

theorem finset.center_mass_filter_ne_zero {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {t : finset ι} {w : ι → } (z : ι → E) :
(finset.filter (λ (i : ι), w i 0) t).center_mass w z = t.center_mass w z

theorem convex.center_mass_mem {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {s : set E} {t : finset ι} {w : ι → } {z : ι → E} :
convex s(∀ (i : ι), i t0 w i)0 < ∑ (i : ι) in t, w i(∀ (i : ι), i tz i s)t.center_mass w z s

Center mass of a finite subset of a convex set belongs to the set provided that all weights are non-negative, and the total weight is positive.

theorem convex.sum_mem {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {s : set E} {t : finset ι} {w : ι → } {z : ι → E} :
convex s(∀ (i : ι), i t0 w i)∑ (i : ι) in t, w i = 1(∀ (i : ι), i tz i s)∑ (i : ι) in t, w i z i s

theorem convex_iff_sum_mem {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex s ∀ (t : finset E) (w : E → ), (∀ (i : E), i t0 w i)∑ (i : E) in t, w i = 1(∀ (x : E), x tx s)∑ (x : E) in t, w x x s

theorem convex_on.map_center_mass_le {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {s : set E} {t : finset ι} {w : ι → } {z : ι → E} {f : E → } :
convex_on s f(∀ (i : ι), i t0 w i)0 < ∑ (i : ι) in t, w i(∀ (i : ι), i tz i s)f (t.center_mass w z) t.center_mass w (f z)

Jensen's inequality, finset.center_mass version.

theorem convex_on.map_sum_le {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {s : set E} {t : finset ι} {w : ι → } {z : ι → E} {f : E → } :
convex_on s f(∀ (i : ι), i t0 w i)∑ (i : ι) in t, w i = 1(∀ (i : ι), i tz i s)f (∑ (i : ι) in t, w i z i) ∑ (i : ι) in t, (w i) * f (z i)

Jensen's inequality, finset.sum version.

theorem convex_on.exists_ge_of_center_mass {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {s : set E} {t : finset ι} {w : ι → } {z : ι → E} {f : E → } :
convex_on s f(∀ (i : ι), i t0 w i)0 < ∑ (i : ι) in t, w i(∀ (i : ι), i tz i s)(∃ (i : ι) (H : i t), f (t.center_mass w z) f (z i))

If a function f is convex on s takes value y at the center mass of some points z i ∈ s, then for some i we have y ≤ f (z i).

def convex_hull {E : Type u} [add_comm_group E] [vector_space E] :
set Eset E

Convex hull of a set s is the minimal convex set that includes s

Equations
theorem subset_convex_hull {E : Type u} [add_comm_group E] [vector_space E] (s : set E) :

theorem convex_convex_hull {E : Type u} [add_comm_group E] [vector_space E] (s : set E) :

theorem convex_hull_min {E : Type u} [add_comm_group E] [vector_space E] {s t : set E} :
s tconvex tconvex_hull s t

theorem convex_hull_mono {E : Type u} [add_comm_group E] [vector_space E] {s t : set E} :

theorem convex.convex_hull_eq {E : Type u} [add_comm_group E] [vector_space E] {s : set E} :
convex sconvex_hull s = s

@[simp]
theorem convex_hull_singleton {E : Type u} [add_comm_group E] [vector_space E] {x : E} :
convex_hull {x} = {x}

theorem is_linear_map.image_convex_hull {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set E} {f : E → F} :

theorem linear_map.image_convex_hull {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {s : set E} (f : E →ₗ[] F) :

theorem finset.center_mass_mem_convex_hull {E : Type u} {ι : Type w} [add_comm_group E] [vector_space E] {s : set E} (t : finset ι) {w : ι → } (hw₀ : ∀ (i : ι), i t0 w i) (hws : 0 < ∑ (i : ι) in t, w i) {z : ι → E} :
(∀ (i : ι), i tz i s)t.center_mass w z convex_hull s

theorem convex_hull_eq {E : Type u} [add_comm_group E] [vector_space E] (s : set E) :
convex_hull s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → ) (z : ι → E) (hw₀ : ∀ (i : ι), i t0 w i) (hw₁ : ∑ (i : ι) in t, w i = 1) (hz : ∀ (i : ι), i tz i s), t.center_mass w z = x}

Convex hull of s is equal to the set of all centers of masses of finsets t, z '' t ⊆ s. This version allows finsets in any type in any universe.

theorem convex_on.exists_ge_of_mem_convex_hull {E : Type u} [add_comm_group E] [vector_space E] {s : set E} {f : E → } (hf : convex_on (convex_hull s) f) {x : E} :
x convex_hull s(∃ (y : E) (H : y s), f x f y)

Maximum principle for convex functions. If a function f is convex on the convex hull of s, then f can't have a maximum on convex_hull s outside of s.

theorem finset.convex_hull_eq {E : Type u} [add_comm_group E] [vector_space E] (s : finset E) :
convex_hull s = {x : E | ∃ (w : E → ) (hw₀ : ∀ (y : E), y s0 w y) (hw₁ : ∑ (y : E) in s, w y = 1), s.center_mass w id = x}

theorem set.finite.convex_hull_eq {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (hs : s.finite) :
convex_hull s = {x : E | ∃ (w : E → ) (hw₀ : ∀ (y : E), y s0 w y) (hw₁ : ∑ (y : E) in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x}

theorem is_linear_map.convex_hull_image {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] {f : E → F} (hf : is_linear_map f) (s : set E) :

theorem linear_map.convex_hull_image {E : Type u} {F : Type v} [add_comm_group E] [vector_space E] [add_comm_group F] [vector_space F] (f : E →ₗ[] F) (s : set E) :

Simplex

def std_simplex (ι : Type u_1) [fintype ι] :
set (ι → )

Standard simplex in the space of functions ι → ℝ is the set of vectors with non-negative coordinates with total sum 1.

Equations
theorem std_simplex_eq_inter (ι : Type w) [fintype ι] :
std_simplex ι = (⋂ (x : ι), {f : ι → | 0 f x}) {f : ι → | ∑ (x : ι), f x = 1}

theorem convex_std_simplex (ι : Type w) [fintype ι] :

theorem ite_eq_mem_std_simplex {ι : Type w} [fintype ι] (i : ι) :
(λ (j : ι), ite (i = j) 1 0) std_simplex ι

theorem convex_hull_basis_eq_std_simplex {ι : Type w} [fintype ι] :
convex_hull (set.range (λ (i j : ι), ite (i = j) 1 0)) = std_simplex ι

std_simplex ι is the convex hull of the canonical basis in ι → ℝ.

theorem set.finite.convex_hull_eq_image {E : Type u} [add_comm_group E] [vector_space E] {s : set E} (hs : s.finite) :

Convex hull of a finite set is the image of the standard simplex in s → ℝ under the linear map sending each function w to ∑ x in s, w x • x.

Since we have no sums over finite sets, we use sum over @finset.univ _ hs.fintype. The map is defined in terms of operations on (s → ℝ) →ₗ[ℝ] ℝ so that later we will not need to prove that this map is linear.

theorem mem_Icc_of_mem_std_simplex {ι : Type w} [fintype ι] {f : ι → } (hf : f std_simplex ι) (x : ι) :
f x set.Icc 0 1

All values of a function f ∈ std_simplex ι belong to [0, 1].