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_module ℝ β.

Notations #

We use the following local notations:

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

Implementation notes #

convex_hull is defined as a closure operator. This gives access to the closure_operator API while the impact on writing code is minimal as convex_hull s is automatically elaborated as ⇑convex_hull s.

Segment #

source
def segment {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
set E

Segments in a vector space.

Equations
source
theorem segment_symm {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
segment x y = segment y x
source
theorem left_mem_segment {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
x ∈ segment x y
source
theorem right_mem_segment {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
y ∈ segment x y
source
theorem segment_same {E : Type u} [add_comm_group E] [module ℝ E] (x : E) :
segment x x = {x}
source
theorem segment_eq_image {E : Type u} [add_comm_group E] [module ℝ 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] [module ℝ 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] [module ℝ 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 : ℝ} (h : 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] [module ℝ 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] [module ℝ 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] [module ℝ E] (a b c : E) :
(λ (x : E), a + x) '' segment b c = segment (a + b) (a + c)
source
theorem segment_image {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] (f : E →ₗ[ℝ] F) (a b : E) :
⇑f '' segment a b = segment (⇑f a) (⇑f b)
source
def open_segment {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
set E

Open segment in a vector space. Note that open_segment x x = {x} instead of being ∅.

Equations
source
theorem open_segment_subset_segment {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
open_segment x y ⊆ segment x y
source
theorem mem_open_segment_of_ne_left_right {E : Type u} [add_comm_group E] [module ℝ E] {x y z : E} (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ segment x y) :
z ∈ open_segment x y
source
theorem open_segment_symm {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
open_segment x y = open_segment y x
source
@[simp]
theorem open_segment_same {E : Type u} [add_comm_group E] [module ℝ E] (x : E) :
open_segment x x = {x}
source
@[simp]
theorem left_mem_open_segment_iff {E : Type u} [add_comm_group E] [module ℝ E] {x y : E} :
x ∈ open_segment x y ↔ x = y
source
@[simp]
theorem right_mem_open_segment_iff {E : Type u} [add_comm_group E] [module ℝ E] {x y : E} :
y ∈ open_segment x y ↔ x = y
source
theorem open_segment_eq_image {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
open_segment x y = (λ (θ : ℝ), (1 - θ) • x + θ • y) '' set.Ioo 0 1
source
theorem open_segment_eq_image' {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
open_segment x y = (λ (θ : ℝ), x + θ • (y - x)) '' set.Ioo 0 1
source
theorem open_segment_eq_image₂ {E : Type u} [add_comm_group E] [module ℝ E] (x y : E) :
open_segment x y = (λ (p : ℝ × ℝ), p.fst • x + p.snd • y) '' {p : ℝ × ℝ | 0 < p.fst ∧ 0 < p.snd ∧ p.fst + p.snd = 1}
source
@[simp]
theorem open_segment_eq_Ioo {a b : ℝ} (h : a < b) :
open_segment a b = set.Ioo a b
source
theorem open_segment_eq_Ioo' {a b : ℝ} (hab : a ≠ b) :
open_segment a b = set.Ioo (min a b) (max a b)
source
@[simp]
theorem mem_open_segment_translate {E : Type u} [add_comm_group E] [module ℝ E] (a : E) {x b c : E} :
a + x ∈ open_segment (a + b) (a + c) ↔ x ∈ open_segment b c
source
@[simp]
theorem open_segment_translate_preimage {E : Type u} [add_comm_group E] [module ℝ E] (a b c : E) :
(λ (x : E), a + x) ⁻¹' open_segment (a + b) (a + c) = open_segment b c
source
theorem open_segment_translate_image {E : Type u} [add_comm_group E] [module ℝ E] (a b c : E) :
(λ (x : E), a + x) '' open_segment b c = open_segment (a + b) (a + c)
source
@[simp]
theorem open_segment_image {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] (f : E →ₗ[ℝ] F) (a b : E) :
⇑f '' open_segment a b = open_segment (⇑f a) (⇑f b)

Convexity of sets #

source
def convex {E : Type u} [add_comm_group E] [module ℝ E] (s : set E) :
Prop

Convexity of sets.

Equations
source
theorem convex_iff_forall_pos {E : Type u} [add_comm_group E] [module ℝ 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] [module ℝ E] {s : set E} :
convex s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → segment x y ⊆ s
source
theorem convex_iff_open_segment_subset {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} :
convex s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → open_segment x y ⊆ s
source
theorem convex.segment_subset {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
segment x y ⊆ s
source
theorem convex.open_segment_subset {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
open_segment x y ⊆ s
source
theorem convex.add_smul_sub_mem {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (h : convex s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : ℝ} (ht : t ∈ set.Icc 0 1) :
x + t • (y - x) ∈ s
source
theorem convex.add_smul_mem {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (h : convex s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : ℝ} (ht : t ∈ set.Icc 0 1) :
x + t • y ∈ s
source
theorem convex.smul_mem_of_zero_mem {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (h : convex s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : ℝ} (ht : t ∈ set.Icc 0 1) :
t • x ∈ s
source
theorem convex.mem_smul_of_zero_mem {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (h : convex s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : ℝ} (ht : 1 ≤ t) :
x ∈ t • s
source
theorem convex_iff_pointwise_add_subset {E : Type u} [add_comm_group E] [module ℝ 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] [module ℝ 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] [module ℝ E] :
convex ∅
source
theorem convex_singleton {E : Type u} [add_comm_group E] [module ℝ E] (c : E) :
convex {c}
source
theorem convex_univ {E : Type u} [add_comm_group E] [module ℝ E] :
convex set.univ
source
theorem convex.inter {E : Type u} [add_comm_group E] [module ℝ E] {s t : set E} (hs : convex s) (ht : convex t) :
convex (s ∩ t)
source
theorem convex_sInter {E : Type u} [add_comm_group E] [module ℝ E] {S : set (set E)} (h : ∀ (s : set E), s ∈ S → convex s) :
convex (⋂₀S)
source
theorem convex_Inter {E : Type u} [add_comm_group E] [module ℝ E] {ι : Sort u_1} {s : ι → set E} (h : ∀ (i : ι), convex (s i)) :
convex (⋂ (i : ι), s i)
source
theorem convex.prod {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set E} {t : set F} (hs : convex s) (ht : convex t) :
convex (s.prod t)
source
theorem directed.convex_Union {E : Type u} [add_comm_group E] [module ℝ E] {ι : Sort u_1} {s : ι → set E} (hdir : directed has_subset.subset s) (hc : ∀ ⦃i : ι⦄, convex (s i)) :
convex (⋃ (i : ι), s i)
source
theorem directed_on.convex_sUnion {E : Type u} [add_comm_group E] [module ℝ E] {c : set (set E)} (hdir : directed_on has_subset.subset c) (hc : ∀ ⦃A : set E⦄, A ∈ c → convex A) :
convex (⋃₀c)
source
theorem convex.combo_to_vadd {E : Type u} [add_comm_group E] [module ℝ E] {a b : ℝ} {x y : E} (h : 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] [module ℝ E] [add_comm_group F] [module ℝ F] {a b : ℝ} {x y : E} {f : E →ᵃ[ℝ] F} (h : 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] [module ℝ E] [add_comm_group F] [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.

source
theorem convex.affine_image {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] (f : E →ᵃ[ℝ] F) {s : set E} (hs : 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] [module ℝ E] [add_comm_group F] [module ℝ 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] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set E} (hs : convex s) {f : E → F} (hf : is_linear_map ℝ f) :
convex (f '' s)
source
theorem convex.linear_preimage {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ 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] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set F} (hs : convex s) {f : E → F} (hf : is_linear_map ℝ f) :
convex (f ⁻¹' s)
source
theorem convex.neg {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex s) :
convex ((λ (z : E), -z) '' s)
source
theorem convex.neg_preimage {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex s) :
convex ((λ (z : E), -z) ⁻¹' s)
source
theorem convex.smul {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (c : ℝ) (hs : convex s) :
convex (c • s)
source
theorem convex.smul_preimage {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (c : ℝ) (hs : convex s) :
convex ((λ (z : E), c • z) ⁻¹' s)
source
theorem convex.add {E : Type u} [add_comm_group E] [module ℝ E] {s t : set E} (hs : convex s) (ht : convex t) :
convex (s + t)
source
theorem convex.sub {E : Type u} [add_comm_group E] [module ℝ E] {s t : set E} (hs : convex s) (ht : convex t) :
convex ((λ (x : E × E), x.fst - x.snd) '' s.prod t)
source
theorem convex.translate {E : Type u} [add_comm_group E] [module ℝ 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] [module ℝ 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] [module ℝ 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] [module ℝ 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 set.ord_connected.convex {s : set ℝ} :
s.ord_connected → convex s

Alias of real.convex_iff_ord_connected.

source
theorem convex.ord_connected {s : set ℝ} :
convex s → s.ord_connected

Alias of real.convex_iff_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] [module ℝ E] (a b : E) :
convex (segment a b)
source
theorem convex_open_segment {E : Type u} [add_comm_group E] [module ℝ E] (a b : E) :
convex (open_segment a b)
source
theorem convex_halfspace_lt {E : Type u} [add_comm_group E] [module ℝ 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] [module ℝ 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] [module ℝ 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] [module ℝ 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] [module ℝ 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}

Convex combinations in intervals #

source
theorem convex.combo_self {α : Type v'} [linear_ordered_field α] (a : α) {x y : α} (h : x + y = 1) :
a = x * a + y * a
source
theorem convex.mem_Ioo {α : Type v'} [linear_ordered_field α] {a b x : α} (h : 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 : α} (h : 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 : α} (h : 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 : α} (h : 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] [module ℝ E] (K : submodule ℝ E) :
convex ↑K
source
theorem subspace.convex {E : Type u} [add_comm_group E] [module ℝ E] (K : subspace ℝ E) :
convex ↑K

Convex and concave functions #

source
def convex_on {E : Type u} [add_comm_group E] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] (s : set E) (f : E → β) :
Prop

Convexity of functions

Equations
source
def concave_on {E : Type u} [add_comm_group E] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] (s : set E) (f : E → β) :
Prop

Concavity of functions

Equations
source
@[simp]
theorem neg_convex_on_iff {E : Type u} [add_comm_group E] [module ℝ E] {γ : Type u_1} [ordered_add_comm_group γ] [module ℝ γ] (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] [module ℝ E] {γ : Type u_1} [ordered_add_comm_group γ] [module ℝ γ] (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 ℝ} (hs : convex s) :
convex_on s id
source
theorem concave_on_id {s : set ℝ} (hs : convex s) :
concave_on s id
source
theorem convex_on_const {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] (c : β) (hs : convex s) :
convex_on s (λ (x : E), c)
source
theorem concave_on_const {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] (c : β) (hs : convex s) :
concave_on s (λ (x : E), c)
source
theorem convex_on_iff_div {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : E → β} [linear_order E] (hs : convex s) (hf : ∀ ⦃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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : E → β} [linear_order E] (hs : convex s) (hf : ∀ ⦃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 : ℝ → ℝ} (hf : ∀ {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 : ℝ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : 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 : ℝ → ℝ} (hf : ∀ {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 : ℝ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : 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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {t : set E} {f : E → β} (h_convex_on : convex_on t f) (h_subset : s ⊆ t) (h_convex : convex s) :
convex_on s f
source
theorem concave_on.subset {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {t : set E} {f : E → β} (h_concave_on : concave_on t f) (h_subset : s ⊆ t) (h_convex : convex s) :
concave_on s f
source
theorem convex_on.add {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f g : E → β} (hf : convex_on s f) (hg : 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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f g : E → β} (hf : concave_on s f) (hg : 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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] [ordered_module ℝ β] {f : E → β} {c : ℝ} (hc : 0 ≤ c) (hf : convex_on s f) :
convex_on s (λ (x : E), c • f x)
source
theorem concave_on.smul {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] [ordered_module ℝ β] {f : E → β} {c : ℝ} (hc : 0 ≤ c) (hf : 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] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : convex_on s f) {x y : E} {a b : ℝ} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 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] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : concave_on s f) {x y : E} {a b : ℝ} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 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] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : convex_on s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : 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] [module ℝ E] {s : set E} {γ : Type u_1} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : concave_on s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : 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.le_left_of_right_le' {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : convex_on s f) {x y : E} {a b : ℝ} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : f y ≤ f (a • x + b • y)) :
f (a • x + b • y) ≤ f x
source
theorem concave_on.left_le_of_le_right' {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : concave_on s f) {x y : E} {a b : ℝ} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : f (a • x + b • y) ≤ f y) :
f x ≤ f (a • x + b • y)
source
theorem convex_on.le_right_of_left_le' {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : convex_on s f) {x y : E} {a b : ℝ} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hxy : f x ≤ f (a • x + b • y)) :
f (a • x + b • y) ≤ f y
source
theorem concave_on.le_right_of_left_le' {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : concave_on s f) {x y : E} {a b : ℝ} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hxy : f (a • x + b • y) ≤ f x) :
f y ≤ f (a • x + b • y)
source
theorem convex_on.le_left_of_right_le {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : convex_on s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment x y) (hyz : f y ≤ f z) :
f z ≤ f x
source
theorem concave_on.left_le_of_le_right {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : concave_on s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment x y) (hyz : f z ≤ f y) :
f x ≤ f z
source
theorem convex_on.le_right_of_left_le {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : convex_on s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment x y) (hxz : f x ≤ f z) :
f z ≤ f y
source
theorem concave_on.le_right_of_left_le {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {γ : Type u_2} [linear_ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : concave_on s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment x y) (hxz : f z ≤ f x) :
f y ≤ f z
source
theorem convex_on.convex_le {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] [ordered_module ℝ β] {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] [module ℝ E] {s : set E} {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] [ordered_module ℝ β] {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] [module ℝ E] {s : set E} {γ : Type u_1} [ordered_cancel_add_comm_monoid γ] [module ℝ γ] [ordered_module ℝ γ] {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] [module ℝ E] {s : set E} {γ : Type u_1} [ordered_cancel_add_comm_monoid γ] [module ℝ γ] [ordered_module ℝ γ] {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] [module ℝ E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : 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] [module ℝ E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} (hf : 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] [module ℝ E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {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] [module ℝ E] {s : set E} {γ : Type u_1} [ordered_add_comm_group γ] [module ℝ γ] [ordered_module ℝ γ] {f : E → γ} :
concave_on s f ↔ convex {p : E × γ | p.fst ∈ s ∧ p.snd ≤ f p.fst}
source
theorem linear_map.convex_on {E : Type u} [add_comm_group E] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] (f : E →ₗ[ℝ] β) {s : set E} (hs : convex s) :
convex_on s ⇑f
source
theorem linear_map.concave_on {E : Type u} [add_comm_group E] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] (f : E →ₗ[ℝ] β) {s : set E} (hs : convex s) :
concave_on s ⇑f
source
theorem convex_on.comp_affine_map {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : F → β} (g : E →ᵃ[ℝ] F) {s : set F} (hf : 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] [module ℝ E] [add_comm_group F] [module ℝ F] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : F → β} (g : E →ᵃ[ℝ] F) {s : set F} (hf : 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] [module ℝ E] [add_comm_group F] [module ℝ F] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {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] [module ℝ E] [add_comm_group F] [module ℝ F] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {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] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : E → β} {s : set E} {a : E} (hf : 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] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : E → β} {s : set E} {a : E} (hf : 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] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : E → β} {s : set E} {a : E} (hf : 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] [module ℝ E] {β : Type u_1} [ordered_add_comm_monoid β] [module ℝ β] {f : E → β} {s : set E} {a : E} (hf : 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.

Center of mass #

source
def finset.center_mass {E : Type u} {ι : Type w} [add_comm_group E] [module ℝ E] (t : finset ι) (w : ι → ℝ) (z : ι → E) :
E

Center of 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] [module ℝ E] (w : ι → ℝ) (z : ι → E) :
∅.center_mass w z = 0
source
theorem finset.center_mass_pair {E : Type u} {ι : Type w} [add_comm_group E] [module ℝ E] (i j : ι) (w : ι → ℝ) (z : ι → E) (hne : 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] [module ℝ E] (i : ι) (t : finset ι) {w : ι → ℝ} (z : ι → E) (ha : i ∉ t) (hw : ∑ (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] [module ℝ E] (i : ι) {w : ι → ℝ} (z : ι → E) (hw : 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] [module ℝ E] (t : finset ι) {w : ι → ℝ} (z : ι → E) (hw : ∑ (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] [module ℝ 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] [module ℝ 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 : ℝ) (hab : a + b = 1) :
a • s.center_mass ws zs + b • t.center_mass wt zt = (finset.map function.embedding.inl s ∪ finset.map function.embedding.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] [module ℝ E] (s : finset ι) (w₁ w₂ : ι → ℝ) (z : ι → E) (hw₁ : ∑ (i : ι) in s, w₁ i = 1) (hw₂ : ∑ (i : ι) in s, w₂ i = 1) (a b : ℝ) (hab : 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] [module ℝ E] (i : ι) (t : finset ι) (z : ι → E) (hi : 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] [module ℝ E] {t : finset ι} {w : ι → ℝ} (z : ι → E) {t' : finset ι} (ht : t ⊆ t') (h : ∀ (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] [module ℝ 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] [module ℝ E] {s : set E} {t : finset ι} {w : ι → ℝ} {z : ι → E} (hs : 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

The center of 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] [module ℝ E] {s : set E} {t : finset ι} {w : ι → ℝ} {z : ι → E} (hs : convex s) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (h₁ : ∑ (i : ι) in t, w i = 1) (hz : ∀ (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] [module ℝ 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] [module ℝ E] {s : set E} {t : finset ι} {w : ι → ℝ} {z : ι → E} {f : E → ℝ} (hf : convex_on s f) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (hpos : 0 < ∑ (i : ι) in t, w i) (hmem : ∀ (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] [module ℝ E] {s : set E} {t : finset ι} {w : ι → ℝ} {z : ι → E} {f : E → ℝ} (hf : convex_on s f) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (h₁ : ∑ (i : ι) in t, w i = 1) (hmem : ∀ (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] [module ℝ E] {s : set E} {t : finset ι} {w : ι → ℝ} {z : ι → E} {f : E → ℝ} (h : convex_on s f) (hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (hws : 0 < ∑ (i : ι) in t, w i) (hz : ∀ (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 of mass of some points z i ∈ s, then for some i we have y ≤ f (z i).

Convex hull #

source
def convex_hull {E : Type u} [add_comm_group E] [module ℝ E] :
closure_operator (set E)

The 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] [module ℝ E] (s : set E) :
s ⊆ ⇑convex_hull s
source
theorem convex_convex_hull {E : Type u} [add_comm_group E] [module ℝ E] (s : set E) :
convex (⇑convex_hull s)
source
theorem convex_hull_min {E : Type u} [add_comm_group E] [module ℝ E] {s t : set E} (hst : s ⊆ t) (ht : convex t) :
⇑convex_hull s ⊆ t
source
theorem convex_hull_mono {E : Type u} [add_comm_group E] [module ℝ E] {s t : set E} (hst : s ⊆ t) :
⇑convex_hull s ⊆ ⇑convex_hull t
source
theorem convex.convex_hull_eq {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex s) :
⇑convex_hull s = s
source
@[simp]
theorem convex_hull_empty {E : Type u} [add_comm_group E] [module ℝ E] :
⇑convex_hull ∅ = ∅
source
@[simp]
theorem convex_hull_empty_iff {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} :
⇑convex_hull s = ∅ ↔ s = ∅
source
@[simp]
theorem convex_hull_nonempty_iff {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} :
(⇑convex_hull s).nonempty ↔ s.nonempty
source
@[simp]
theorem convex_hull_singleton {E : Type u} [add_comm_group E] [module ℝ E] {x : E} :
⇑convex_hull {x} = {x}
source
theorem convex.convex_remove_iff_not_mem_convex_hull_remove {E : Type u} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex s) (x : E) :
convex (s \ {x}) ↔ x ∉ ⇑convex_hull (s \ {x})
source
theorem is_linear_map.image_convex_hull {E : Type u} {F : Type v} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set E} {f : E → F} (hf : 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] [module ℝ E] [add_comm_group F] [module ℝ 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] [module ℝ E] {s : set E} (t : finset ι) {w : ι → ℝ} (hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (hws : 0 < ∑ (i : ι) in t, w i) {z : ι → E} (hz : ∀ (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] [module ℝ 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] [module ℝ E] {s : set E} {f : E → ℝ} (hf : convex_on (⇑convex_hull s) f) {x : E} (hx : 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] [module ℝ 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] [module ℝ 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] [module ℝ 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] [module ℝ E] [add_comm_group F] [module ℝ 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] [module ℝ E] [add_comm_group F] [module ℝ 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 (ι → ℝ)

The 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] [module ℝ E] {s : set E} (hs : s.finite) :
⇑convex_hull s = (⇑∑ (x : ↥s), (linear_map.proj x).smul_right x.val) '' std_simplex ↥s

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