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

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

Segments in a vector space

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

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

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

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

source
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

source
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

source
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}

source
theorem segment_eq_Icc {a b : ℝ} :
a ≤ b → segment a b = set.Icc a b

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

source
theorem segment_eq_interval (a b : ℝ) :
segment a b = set.interval a b

source
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

source
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

source
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

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

Convexity of sets

Equations
source
theorem convex_iff_forall_pos {E : Type u} [add_comm_group E] [vector_space ℝ E] {s : set E} :
convex s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

source
theorem convex_iff_segment_subset {E : Type u} [add_comm_group E] [vector_space ℝ E] {s : set E} :
convex s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → segment x y ⊆ s

source
theorem convex.segment_subset {E : Type u} [add_comm_group E] [vector_space ℝ E] {s : set E} (h : convex s) {x y : E} :
x ∈ s → y ∈ s → segment x y ⊆ s

source
theorem convex_iff_pointwise_add_subset {E : Type u} [add_comm_group E] [vector_space ℝ 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.

source
theorem convex_iff_div {E : Type u} [add_comm_group E] [vector_space ℝ E] {s : set E} :
convex s ↔ ∀ ⦃x y : E⦄, x ∈ s → 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

Examples of convex sets

source
theorem convex_empty {E : Type u} [add_comm_group E] [vector_space ℝ E] :
convex ∅

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

source
theorem convex_univ {E : Type u} [add_comm_group E] [vector_space ℝ E] :
convex set.univ

source
theorem convex.inter {E : Type u} [add_comm_group E] [vector_space ℝ E] {s t : set E} :
convex s → convex t → convex (s ∩ t)

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

source
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)

source
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 s → convex t → convex (s.prod t)

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

source
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 = 1 → ⇑f (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.

source
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 s → convex (⇑f ⁻¹' s)

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

source
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 s → convex (⇑f '' s)

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

source
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) :
convex (⇑f '' s)

source
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} :
is_linear_map ℝ f → convex (f '' s)

source
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) :
convex (⇑f ⁻¹' s)

source
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} :
is_linear_map ℝ f → convex (f ⁻¹' s)

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

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

source
theorem convex.smul {E : Type u} [add_comm_group E] [vector_space ℝ E] {s : set E} (c : ℝ) :
convex s → convex (c • s)

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

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

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

source
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)

source
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

source
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

source
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)

source
theorem real.convex_iff_ord_connected {s : set ℝ} :
convex s ↔ s.ord_connected

source
theorem convex_Iio (r : ℝ) :
convex (set.Iio r)

source
theorem convex_Ioi (r : ℝ) :
convex (set.Ioi r)

source
theorem convex_Iic (r : ℝ) :
convex (set.Iic r)

source
theorem convex_Ici (r : ℝ) :
convex (set.Ici r)

source
theorem convex_Ioo (r s : ℝ) :
convex (set.Ioo r s)

source
theorem convex_Ico (r s : ℝ) :
convex (set.Ico r s)

source
theorem convex_Ioc (r s : ℝ) :
convex (set.Ioc r s)

source
theorem convex_Icc (r s : ℝ) :
convex (set.Icc r s)

source
theorem convex_interval (r s : ℝ) :
convex (set.interval r s)

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

source
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}

source
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}

source
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}

source
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}

source
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}

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

source
theorem convex_halfspace_re_le (r : ℝ) :
convex {c : ℂ | c.re ≤ r}

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

source
theorem convex_halfspace_re_lge (r : ℝ) :
convex {c : ℂ | r ≤ c.re}

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

source
theorem convex_halfspace_im_le (r : ℝ) :
convex {c : ℂ | c.im ≤ r}

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

source
theorem convex_halfspace_im_lge (r : ℝ) :
convex {c : ℂ | r ≤ c.im}

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

source
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.

source
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.

source
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.

source
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.

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

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

Convex functions

source
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
source
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
source
@[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 → γ) :
convex_on s (-f) ↔ concave_on s f

A function f is concave iff -f is convex

source
@[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 → γ) :
concave_on s (-f) ↔ convex_on s f

A function f is concave iff -f is convex

source
theorem convex_on_id {s : set ℝ} :
convex s → convex_on s id

source
theorem concave_on_id {s : set ℝ} :
convex s → concave_on s id

source
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 s → convex_on s (λ (x : E), c)

source
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 s → concave_on s (λ (x : E), c)

source
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 ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y

source
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 ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)

source
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 ∈ s → y ∈ s → x < y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → f (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.

source
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 ∈ s → y ∈ s → x < y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • 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.

source
theorem convex_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex s) {f : ℝ → ℝ} :
(∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < 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.

source
theorem convex_on.slope_mono_adjacent {s : set ℝ} {f : ℝ → ℝ} (hf : convex_on s f) {x y z : ℝ} :
x ∈ s → z ∈ s → x < y → y < 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].

source
theorem convex_on_real_iff_slope_mono_adjacent {s : set ℝ} (hs : convex s) {f : ℝ → ℝ} :
convex_on s f ↔ ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < 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].

source
theorem concave_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex s) {f : ℝ → ℝ} :
(∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < 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.

source
theorem concave_on.slope_mono_adjacent {s : set ℝ} {f : ℝ → ℝ} (hf : concave_on s f) {x y z : ℝ} :
x ∈ s → z ∈ s → x < y → y < 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].

source
theorem concave_on_real_iff_slope_mono_adjacent {s : set ℝ} (hs : convex s) {f : ℝ → ℝ} :
concave_on s f ↔ ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < 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].

source
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 f → s ⊆ t → convex s → convex_on s f

source
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 f → s ⊆ t → convex s → concave_on s f

source
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 f → convex_on s g → convex_on s (λ (x : E), f x + g x)

source
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 f → concave_on s g → concave_on s (λ (x : E), f x + g x)

source
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 ≤ c → convex_on s f → convex_on s (λ (x : E), c • f x)

source
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 ≤ c → concave_on s f → concave_on s (λ (x : E), c • f x)

source
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 f → x ∈ s → y ∈ s → 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)

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

source
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 f → x ∈ s → y ∈ s → 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)

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

source
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 ∈ s → y ∈ s → z ∈ segment x y → f z ≤ max (f x) (f y)

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

source
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 ∈ s → y ∈ s → z ∈ segment x y → min (f x) (f y) ≤ f z

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

source
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}

source
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}

source
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}

source
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}

source
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 f → convex {p : E × γ | p.fst ∈ s ∧ f p.fst ≤ p.snd}

source
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 f → convex {p : E × γ | p.fst ∈ s ∧ p.snd ≤ f p.fst}

source
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}

source
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}

source
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 f → convex_on (⇑g ⁻¹' s) (f ∘ ⇑g)

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

source
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} :
concave_on s f → concave_on (⇑g ⁻¹' s) (f ∘ ⇑g)

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

source
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) :
convex_on (⇑f ⁻¹' s) (g ∘ ⇑f)

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

source
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) :
concave_on (⇑f ⁻¹' s) (g ∘ ⇑f)

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

source
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 f → convex_on ((λ (z : E), a + z) ⁻¹' s) (f ∘ λ (z : E), a + z)

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

source
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 f → concave_on ((λ (z : E), a + z) ⁻¹' s) (f ∘ λ (z : E), a + z)

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

source
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 f → convex_on ((λ (z : E), a + z) ⁻¹' s) (f ∘ λ (z : E), z + a)

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

source
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 f → concave_on ((λ (z : E), a + z) ⁻¹' s) (f ∘ λ (z : E), z + a)

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

source
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
source
theorem finset.center_mass_empty {E : Type u} {ι : Type w} [add_comm_group E] [vector_space ℝ E] (w : ι → ℝ) (z : ι → E) :
∅.center_mass w z = 0

source
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

source
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

source
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

source
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 = 1 → t.center_mass w z = ∑ (i : ι) in t, w i • z i

source
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

source
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 = 1 → a • 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.

source
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 = 1 → a • 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.

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

source
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 ∉ t → w i = 0) → t.center_mass w z = t'.center_mass w z

source
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

source
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 ∈ t → 0 ≤ w i) → 0 < ∑ (i : ι) in t, w i → (∀ (i : ι), i ∈ t → z 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.

source
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 ∈ t → 0 ≤ w i) → ∑ (i : ι) in t, w i = 1 → (∀ (i : ι), i ∈ t → z i ∈ s) → ∑ (i : ι) in t, w i • z i ∈ s

source
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 ∈ t → 0 ≤ w i) → ∑ (i : E) in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ (x : E) in t, w x • x ∈ s

source
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 ∈ t → 0 ≤ w i) → 0 < ∑ (i : ι) in t, w i → (∀ (i : ι), i ∈ t → z i ∈ s) → f (t.center_mass w z) ≤ t.center_mass w (f ∘ z)

Jensen's inequality, finset.center_mass version.

source
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 ∈ t → 0 ≤ w i) → ∑ (i : ι) in t, w i = 1 → (∀ (i : ι), i ∈ t → z i ∈ s) → f (∑ (i : ι) in t, w i • z i) ≤ ∑ (i : ι) in t, (w i) * f (z i)

Jensen's inequality, finset.sum version.

source
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 ∈ t → 0 ≤ w i) → 0 < ∑ (i : ι) in t, w i → (∀ (i : ι), i ∈ t → z 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).

source
def convex_hull {E : Type u} [add_comm_group E] [vector_space ℝ E] :
set E → set E

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

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

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

source
theorem convex_hull_min {E : Type u} [add_comm_group E] [vector_space ℝ E] {s t : set E} :
s ⊆ t → convex t → convex_hull s ⊆ t

source
theorem convex_hull_mono {E : Type u} [add_comm_group E] [vector_space ℝ E] {s t : set E} :
s ⊆ t → convex_hull s ⊆ convex_hull t

source
theorem convex.convex_hull_eq {E : Type u} [add_comm_group E] [vector_space ℝ E] {s : set E} :
convex s → convex_hull s = s

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

source
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} :
is_linear_map ℝ f → f '' convex_hull s = convex_hull (f '' s)

source
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) :
⇑f '' convex_hull s = convex_hull (⇑f '' s)

source
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 ∈ t → 0 ≤ w i) (hws : 0 < ∑ (i : ι) in t, w i) {z : ι → E} :
(∀ (i : ι), i ∈ t → z i ∈ s) → t.center_mass w z ∈ convex_hull s

source
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 ∈ t → 0 ≤ w i) (hw₁ : ∑ (i : ι) in t, w i = 1) (hz : ∀ (i : ι), i ∈ t → z 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.

source
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.

source
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 ∈ s → 0 ≤ w y) (hw₁ : ∑ (y : E) in s, w y = 1), s.center_mass w id = x}

source
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 ∈ s → 0 ≤ w y) (hw₁ : ∑ (y : E) in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x}

source
theorem convex_hull_eq_union_convex_hull_finite_subsets {E : Type u} [add_comm_group E] [vector_space ℝ E] (s : set E) :
convex_hull s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull ↑t

source
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) :
convex_hull (f '' s) = f '' convex_hull s

source
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) :
convex_hull (⇑f '' s) = ⇑f '' convex_hull s

Simplex

source
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
source
theorem std_simplex_eq_inter (ι : Type w) [fintype ι] :
std_simplex ι = (⋂ (x : ι), {f : ι → ℝ | 0 ≤ f x}) ∩ {f : ι → ℝ | ∑ (x : ι), f x = 1}

source
theorem convex_std_simplex (ι : Type w) [fintype ι] :
convex (std_simplex ι)

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

source
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 ι → ℝ.

source
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 s = (⇑∑ (x : ↥s), (linear_map.proj x).smul_right x.val) '' std_simplex ↥s

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.

source
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].