mathlib documentation

analysis.convex.basic

Convex sets and functions in vector spaces #

In a π•œ-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.

Notations #

We provide the following notation:

TODO #

Generalize all this file to affine spaces.

Should we rename segment and open_segment to convex.Icc and convex.Ioo? Should we also define clopen_segment/convex.Ico/convex.Ioc?

Segment #

def segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x y : E) :
set E

Segments in a vector space.

Equations
def open_segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x y : E) :
set E

Open segment in a vector space. Note that open_segment π•œ x x = {x} instead of being βˆ… when the base semiring has some element between 0 and 1.

Equations
theorem segment_symm (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x y : E) :
[x -[π•œ] y] = [y -[π•œ] x]
theorem open_segment_symm (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x y : E) :
open_segment π•œ x y = open_segment π•œ y x
theorem open_segment_subset_segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x y : E) :
open_segment π•œ x y βŠ† [x -[π•œ] y]
theorem left_mem_segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [mul_action_with_zero π•œ E] (x y : E) :
x ∈ [x -[π•œ] y]
theorem right_mem_segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [mul_action_with_zero π•œ E] (x y : E) :
y ∈ [x -[π•œ] y]
theorem segment_same (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (x : E) :
[x -[π•œ] x] = {x}
theorem mem_open_segment_of_ne_left_right (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {x y z : E} (hx : x β‰  z) (hy : y β‰  z) (hz : z ∈ [x -[π•œ] y]) :
z ∈ open_segment π•œ x y
theorem open_segment_subset_iff_segment_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {x y : E} {s : set E} (hx : x ∈ s) (hy : y ∈ s) :
open_segment π•œ x y βŠ† s ↔ [x -[π•œ] y] βŠ† s
theorem convex.combo_self {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {a b : π•œ} (h : a + b = 1) (x : E) :
a β€’ x + b β€’ x = x
@[simp]
theorem open_segment_same (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] [nontrivial π•œ] [densely_ordered π•œ] (x : E) :
open_segment π•œ x x = {x}
theorem segment_eq_image (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
[x -[π•œ] y] = (Ξ» (ΞΈ : π•œ), (1 - ΞΈ) β€’ x + ΞΈ β€’ y) '' set.Icc 0 1
theorem open_segment_eq_image (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
open_segment π•œ x y = (Ξ» (ΞΈ : π•œ), (1 - ΞΈ) β€’ x + ΞΈ β€’ y) '' set.Ioo 0 1
theorem segment_eq_imageβ‚‚ (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
[x -[π•œ] y] = (Ξ» (p : π•œ Γ— π•œ), p.fst β€’ x + p.snd β€’ y) '' {p : π•œ Γ— π•œ | 0 ≀ p.fst ∧ 0 ≀ p.snd ∧ p.fst + p.snd = 1}
theorem open_segment_eq_imageβ‚‚ (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [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}
theorem segment_eq_image' (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
[x -[π•œ] y] = (Ξ» (ΞΈ : π•œ), x + ΞΈ β€’ (y - x)) '' set.Icc 0 1
theorem open_segment_eq_image' (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
open_segment π•œ x y = (Ξ» (ΞΈ : π•œ), x + ΞΈ β€’ (y - x)) '' set.Ioo 0 1
theorem segment_image (π•œ : Type u_1) {E : Type u_2} {F : Type u_3} [ordered_ring π•œ] [add_comm_group E] [add_comm_group F] [module π•œ E] [module π•œ F] (f : E β†’β‚—[π•œ] F) (a b : E) :
⇑f '' [a -[π•œ] b] = [⇑f a -[π•œ] ⇑f b]
@[simp]
theorem open_segment_image (π•œ : Type u_1) {E : Type u_2} {F : Type u_3} [ordered_ring π•œ] [add_comm_group E] [add_comm_group F] [module π•œ E] [module π•œ F] (f : E β†’β‚—[π•œ] F) (a b : E) :
⇑f '' open_segment π•œ a b = open_segment π•œ (⇑f a) (⇑f b)
theorem mem_segment_translate (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (a : E) {x b c : E} :
a + x ∈ [a + b -[π•œ] a + c] ↔ x ∈ [b -[π•œ] c]
@[simp]
theorem mem_open_segment_translate (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [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
theorem segment_translate_preimage (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (a b c : E) :
(Ξ» (x : E), a + x) ⁻¹' [a + b -[π•œ] a + c] = [b -[π•œ] c]
theorem open_segment_translate_preimage (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (a b c : E) :
(Ξ» (x : E), a + x) ⁻¹' open_segment π•œ (a + b) (a + c) = open_segment π•œ b c
theorem segment_translate_image (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (a b c : E) :
(Ξ» (x : E), a + x) '' [b -[π•œ] c] = [a + b -[π•œ] a + c]
theorem open_segment_translate_image (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (a b c : E) :
(Ξ» (x : E), a + x) '' open_segment π•œ b c = open_segment π•œ (a + b) (a + c)
@[simp]
theorem left_mem_open_segment_iff {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] [no_zero_smul_divisors π•œ E] {x y : E} :
x ∈ open_segment π•œ x y ↔ x = y
@[simp]
theorem right_mem_open_segment_iff {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {x y : E} :
y ∈ open_segment π•œ x y ↔ x = y

Segments in an ordered space #

Relates segment, open_segment and set.Icc, set.Ico, set.Ioc, set.Ioo

theorem segment_subset_Icc {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [ordered_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] {x y : E} (h : x ≀ y) :
[x -[π•œ] y] βŠ† set.Icc x y
theorem open_segment_subset_Ioo {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [ordered_cancel_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] {x y : E} (h : x < y) :
open_segment π•œ x y βŠ† set.Ioo x y
theorem segment_subset_interval {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] (x y : E) :
[x -[π•œ] y] βŠ† [x, y]
theorem convex.min_le_combo {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] (x y : E) {a b : π•œ} (ha : 0 ≀ a) (hb : 0 ≀ b) (hab : a + b = 1) :
theorem convex.combo_le_max {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] (x y : E) {a b : π•œ} (ha : 0 ≀ a) (hb : 0 ≀ b) (hab : a + b = 1) :
theorem Icc_subset_segment {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} :
set.Icc x y βŠ† [x -[π•œ] y]
@[simp]
theorem segment_eq_Icc {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x ≀ y) :
[x -[π•œ] y] = set.Icc x y
theorem Ioo_subset_open_segment {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} :
set.Ioo x y βŠ† open_segment π•œ x y
@[simp]
theorem open_segment_eq_Ioo {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x < y) :
open_segment π•œ x y = set.Ioo x y
theorem segment_eq_Icc' {π•œ : Type u_1} [linear_ordered_field π•œ] (x y : π•œ) :
[x -[π•œ] y] = set.Icc (min x y) (max x y)
theorem open_segment_eq_Ioo' {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (hxy : x β‰  y) :
open_segment π•œ x y = set.Ioo (min x y) (max x y)
theorem segment_eq_interval {π•œ : Type u_1} [linear_ordered_field π•œ] (x y : π•œ) :
[x -[π•œ] y] = [x, y]
theorem convex.mem_Icc {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x ≀ y) {z : π•œ} :
z ∈ set.Icc x y ↔ βˆƒ (a b : π•œ), 0 ≀ a ∧ 0 ≀ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Icc iff it can be expressed as a convex combination of the endpoints.

theorem convex.mem_Ioo {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x < y) {z : π•œ} :
z ∈ set.Ioo x y ↔ βˆƒ (a b : π•œ), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioo iff it can be expressed as a strict convex combination of the endpoints.

theorem convex.mem_Ioc {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x < y) {z : π•œ} :
z ∈ set.Ioc x y ↔ βˆƒ (a b : π•œ), 0 ≀ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioc iff it can be expressed as a semistrict convex combination of the endpoints.

theorem convex.mem_Ico {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x < y) {z : π•œ} :
z ∈ set.Ico x y ↔ βˆƒ (a b : π•œ), 0 < a ∧ 0 ≀ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ico iff it can be expressed as a semistrict convex combination of the endpoints.

Convexity of sets #

def convex (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (s : set E) :
Prop

Convexity of sets.

Equations
theorem convex_iff_segment_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {s : set E} :
convex π•œ s ↔ βˆ€ ⦃x y : E⦄, x ∈ s β†’ y ∈ s β†’ [x -[π•œ] y] βŠ† s
theorem convex.segment_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {s : set E} (h : convex π•œ s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
[x -[π•œ] y] βŠ† s
theorem convex.open_segment_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {s : set E} (h : convex π•œ s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
open_segment π•œ x y βŠ† s
theorem convex_iff_pointwise_add_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {s : set E} :
convex π•œ s ↔ βˆ€ ⦃a b : π•œβ¦„, 0 ≀ a β†’ 0 ≀ b β†’ a + b = 1 β†’ a β€’ s + b β€’ s βŠ† s

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

theorem convex_empty {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
convex π•œ βˆ…
theorem convex_univ {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
convex π•œ set.univ
theorem convex.inter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {s t : set E} (hs : convex π•œ s) (ht : convex π•œ t) :
convex π•œ (s ∩ t)
theorem convex_sInter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {S : set (set E)} (h : βˆ€ (s : set E), s ∈ S β†’ convex π•œ s) :
convex π•œ (β‹‚β‚€S)
theorem convex_Inter {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {ΞΉ : Sort u_3} {s : ΞΉ β†’ set E} (h : βˆ€ (i : ΞΉ), convex π•œ (s i)) :
convex π•œ (β‹‚ (i : ΞΉ), s i)
theorem convex.prod {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [has_scalar π•œ E] [has_scalar π•œ F] {s : set E} {t : set F} (hs : convex π•œ s) (ht : convex π•œ t) :
convex π•œ (s.prod t)
theorem directed.convex_Union {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {ΞΉ : Sort u_3} {s : ΞΉ β†’ set E} (hdir : directed has_subset.subset s) (hc : βˆ€ ⦃i : ι⦄, convex π•œ (s i)) :
convex π•œ (⋃ (i : ΞΉ), s i)
theorem directed_on.convex_sUnion {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] {c : set (set E)} (hdir : directed_on has_subset.subset c) (hc : βˆ€ ⦃A : set E⦄, A ∈ c β†’ convex π•œ A) :
convex π•œ (⋃₀c)
theorem convex_iff_forall_pos {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid 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
theorem convex_iff_pairwise_on_pos {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} :
convex π•œ s ↔ s.pairwise_on (Ξ» (x y : E), βˆ€ ⦃a b : π•œβ¦„, 0 < a β†’ 0 < b β†’ a + b = 1 β†’ a β€’ x + b β€’ y ∈ s)
theorem convex_iff_open_segment_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} :
convex π•œ s ↔ βˆ€ ⦃x y : E⦄, x ∈ s β†’ y ∈ s β†’ open_segment π•œ x y βŠ† s
theorem convex_singleton {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (c : E) :
convex π•œ {c}
theorem convex.linear_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set E} (hs : convex π•œ s) (f : E β†’β‚—[π•œ] F) :
convex π•œ (⇑f '' s)
theorem convex.is_linear_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set E} (hs : convex π•œ s) {f : E β†’ F} (hf : is_linear_map π•œ f) :
convex π•œ (f '' s)
theorem convex.linear_preimage {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set F} (hs : convex π•œ s) (f : E β†’β‚—[π•œ] F) :
convex π•œ (⇑f ⁻¹' s)
theorem convex.is_linear_preimage {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring π•œ] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set F} (hs : convex π•œ s) {f : E β†’ F} (hf : is_linear_map π•œ f) :
convex π•œ (f ⁻¹' s)
theorem convex.add {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s t : set E} (hs : convex π•œ s) (ht : convex π•œ t) :
convex π•œ (s + t)
theorem convex.translate {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (z : E) :
convex π•œ ((Ξ» (x : E), z + x) '' s)
theorem convex.translate_preimage_right {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (z : E) :
convex π•œ ((Ξ» (x : E), z + x) ⁻¹' s)

The translation of a convex set is also convex.

theorem convex.translate_preimage_left {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (z : E) :
convex π•œ ((Ξ» (x : E), x + z) ⁻¹' s)

The translation of a convex set is also convex.

theorem convex_Iic {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
convex π•œ (set.Iic r)
theorem convex_Ici {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
convex π•œ (set.Ici r)
theorem convex_Icc {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
convex π•œ (set.Icc r s)
theorem convex_halfspace_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] [ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] {f : E β†’ Ξ²} (h : is_linear_map π•œ f) (r : Ξ²) :
convex π•œ {w : E | f w ≀ r}
theorem convex_halfspace_ge {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] [ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] {f : E β†’ Ξ²} (h : is_linear_map π•œ f) (r : Ξ²) :
convex π•œ {w : E | r ≀ f w}
theorem convex_hyperplane {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] [ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] {f : E β†’ Ξ²} (h : is_linear_map π•œ f) (r : Ξ²) :
convex π•œ {w : E | f w = r}
theorem convex_Iio {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
convex π•œ (set.Iio r)
theorem convex_Ioi {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
convex π•œ (set.Ioi r)
theorem convex_Ioo {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
convex π•œ (set.Ioo r s)
theorem convex_Ico {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
convex π•œ (set.Ico r s)
theorem convex_Ioc {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
convex π•œ (set.Ioc r s)
theorem convex_halfspace_lt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] {f : E β†’ Ξ²} (h : is_linear_map π•œ f) (r : Ξ²) :
convex π•œ {w : E | f w < r}
theorem convex_halfspace_gt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] [ordered_cancel_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] {f : E β†’ Ξ²} (h : is_linear_map π•œ f) (r : Ξ²) :
convex π•œ {w : E | r < f w}
theorem convex_interval {π•œ : Type u_1} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
convex π•œ [r, s]
theorem monotone_on.convex_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : monotone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | f x ≀ r}
theorem monotone_on.convex_lt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : monotone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | f x < r}
theorem monotone_on.convex_ge {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : monotone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | r ≀ f x}
theorem monotone_on.convex_gt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : monotone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | r < f x}
theorem antitone_on.convex_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : antitone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | f x ≀ r}
theorem antitone_on.convex_lt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : antitone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | f x < r}
theorem antitone_on.convex_ge {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : antitone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | r ≀ f x}
theorem antitone_on.convex_gt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {s : set E} {f : E β†’ Ξ²} (hf : antitone_on f s) (hs : convex π•œ s) (r : Ξ²) :
convex π•œ {x ∈ s | r < f x}
theorem monotone.convex_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : monotone f) (r : Ξ²) :
convex π•œ {x : E | f x ≀ r}
theorem monotone.convex_lt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : monotone f) (r : Ξ²) :
convex π•œ {x : E | f x ≀ r}
theorem monotone.convex_ge {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : monotone f) (r : Ξ²) :
convex π•œ {x : E | r ≀ f x}
theorem monotone.convex_gt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : monotone f) (r : Ξ²) :
convex π•œ {x : E | f x ≀ r}
theorem antitone.convex_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : antitone f) (r : Ξ²) :
convex π•œ {x : E | f x ≀ r}
theorem antitone.convex_lt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : antitone f) (r : Ξ²) :
convex π•œ {x : E | f x < r}
theorem antitone.convex_ge {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : antitone f) (r : Ξ²) :
convex π•œ {x : E | r ≀ f x}
theorem antitone.convex_gt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid Ξ²] [module π•œ E] [ordered_smul π•œ E] {f : E β†’ Ξ²} (hf : antitone f) (r : Ξ²) :
convex π•œ {x : E | r < f x}
theorem convex.combo_eq_vadd {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [module π•œ E] {a b : π•œ} {x y : E} (h : a + b = 1) :
a β€’ x + b β€’ y = b β€’ (y - x) + x
theorem convex.sub {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [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)
theorem convex_segment {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
convex π•œ [x -[π•œ] y]
theorem convex_open_segment {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [module π•œ E] (a b : E) :
convex π•œ (open_segment π•œ a b)
theorem convex.smul {π•œ : Type u_1} {E : Type u_2} [ordered_comm_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (c : π•œ) :
convex π•œ (c β€’ s)
theorem convex.smul_preimage {π•œ : Type u_1} {E : Type u_2} [ordered_comm_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (c : π•œ) :
convex π•œ ((Ξ» (z : E), c β€’ z) ⁻¹' s)
theorem convex.affinity {π•œ : Type u_1} {E : Type u_2} [ordered_comm_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : convex π•œ s) (z : E) (c : π•œ) :
convex π•œ ((Ξ» (x : E), z + c β€’ x) '' s)
theorem convex.add_smul_mem {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : π•œ} (ht : t ∈ set.Icc 0 1) :
x + t β€’ y ∈ s
theorem convex.smul_mem_of_zero_mem {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : π•œ} (ht : t ∈ set.Icc 0 1) :
theorem convex.add_smul_sub_mem {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [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
theorem affine_subspace.convex {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (Q : affine_subspace π•œ E) :
convex π•œ ↑Q

Affine subspaces are convex.

theorem convex.combo_affine_apply {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring π•œ] [add_comm_group E] [add_comm_group F] [module π•œ E] [module π•œ F] {a b : π•œ} {x y : E} {f : E →ᡃ[π•œ] F} (h : a + b = 1) :

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

theorem convex.affine_preimage {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring π•œ] [add_comm_group E] [add_comm_group F] [module π•œ E] [module π•œ F] (f : E →ᡃ[π•œ] F) {s : set F} (hs : convex π•œ s) :
convex π•œ (⇑f ⁻¹' s)

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

theorem convex.affine_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring π•œ] [add_comm_group E] [add_comm_group F] [module π•œ E] [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.

theorem convex.neg {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) :
convex π•œ ((Ξ» (z : E), -z) '' s)
theorem convex.neg_preimage {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) :
convex π•œ ((Ξ» (z : E), -z) ⁻¹' s)
theorem convex_iff_div {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [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.

theorem convex.mem_smul_of_zero_mem {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [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) :
theorem convex.add_smul {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] {s : set E} (h_conv : convex π•œ s) {p q : π•œ} (hp : 0 ≀ p) (hq : 0 ≀ q) :
(p + q) β€’ s = p β€’ s + q β€’ s

Convex sets in an ordered space #

Relates convex and ord_connected.

theorem set.ord_connected.convex_of_chain {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [ordered_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] {s : set E} (hs : s.ord_connected) (h : zorn.chain has_le.le s) :
convex π•œ s
theorem set.ord_connected.convex {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [linear_ordered_add_comm_monoid E] [module π•œ E] [ordered_smul π•œ E] {s : set E} (hs : s.ord_connected) :
convex π•œ s
theorem convex_iff_ord_connected {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} :
theorem convex.ord_connected {π•œ : Type u_1} [linear_ordered_field π•œ] {s : set π•œ} :
convex π•œ s β†’ s.ord_connected

Alias of convex_iff_ord_connected.

Convexity of submodules/subspaces #

theorem submodule.convex {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (K : submodule π•œ E) :
convex π•œ ↑K
theorem subspace.convex {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] (K : subspace π•œ E) :
convex π•œ ↑K

Simplex #

def std_simplex (π•œ : Type u_1) (ΞΉ : Type u_5) [ordered_semiring π•œ] [fintype ΞΉ] :
set (ΞΉ β†’ π•œ)

The standard simplex in the space of functions ΞΉ β†’ π•œ is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

Equations
theorem std_simplex_eq_inter (π•œ : Type u_1) (ΞΉ : Type u_5) [ordered_semiring π•œ] [fintype ΞΉ] :
std_simplex π•œ ΞΉ = (β‹‚ (x : ΞΉ), {f : ΞΉ β†’ π•œ | 0 ≀ f x}) ∩ {f : ΞΉ β†’ π•œ | βˆ‘ (x : ΞΉ), f x = 1}
theorem convex_std_simplex (π•œ : Type u_1) (ΞΉ : Type u_5) [ordered_semiring π•œ] [fintype ΞΉ] :
convex π•œ (std_simplex π•œ ΞΉ)
theorem ite_eq_mem_std_simplex (π•œ : Type u_1) {ΞΉ : Type u_5} [ordered_semiring π•œ] [fintype ΞΉ] (i : ΞΉ) :
(Ξ» (j : ΞΉ), ite (i = j) 1 0) ∈ std_simplex π•œ ΞΉ