Topological and metric properties of convex sets #

We prove the following facts:

convex.interior : interior of a convex set is convex;
convex.closure : closure of a convex set is convex;
set.finite.compact_convex_hull : convex hull of a finite set is compact;
set.finite.is_closed_convex_hull : convex hull of a finite set is closed;
convex_on_norm, convex_on_dist : norm and distance to a fixed point is convex on any convex set;
convex_on_univ_norm, convex_on_univ_dist : norm and distance to a fixed point is convex on the whole space;
convex_hull_ediam, convex_hull_diam : convex hull of a set has the same (e)metric diameter as the original set;
bounded_convex_hull : convex hull of a set is bounded if and only if the original set is bounded.
bounded_std_simplex, is_closed_std_simplex, compact_std_simplex: topological properties of the standard simplex;

source

theorem real.convex_iff_is_preconnected {s : set ℝ} :

convex ℝ s ↔ is_preconnected s

source

theorem is_preconnected.convex {s : set ℝ} :

is_preconnected s → convex ℝ s

Alias of the reverse direction of real.convex_iff_is_preconnected.

Standard simplex #

source

theorem std_simplex_subset_closed_ball {ι : Type u_1} [fintype ι] :

std_simplex ℝ ι ⊆ metric.closed_ball 0 1

Every vector in std_simplex 𝕜 ι has max-norm at most 1.

source

theorem bounded_std_simplex (ι : Type u_1) [fintype ι] :

metric.bounded (std_simplex ℝ ι)

std_simplex ℝ ι is bounded.

source

theorem is_closed_std_simplex (ι : Type u_1) [fintype ι] :

is_closed (std_simplex ℝ ι)

std_simplex ℝ ι is closed.

source

theorem compact_std_simplex (ι : Type u_1) [fintype ι] :

is_compact (std_simplex ℝ ι)

std_simplex ℝ ι is compact.

Topological vector space #

source

theorem convex.combo_interior_closure_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :

a • interior s + b • closure s ⊆ interior s

If s is a convex set, then a • interior s + b • closure s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also convex.combo_interior_self_subset_interior for a weaker version.

source

theorem convex.combo_interior_self_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :

a • interior s + b • s ⊆ interior s

If s is a convex set, then a • interior s + b • s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also convex.combo_interior_closure_subset_interior for a stronger version.

source

theorem convex.combo_closure_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :

a • closure s + b • interior s ⊆ interior s

If s is a convex set, then a • closure s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also convex.combo_self_interior_subset_interior for a weaker version.

source

theorem convex.combo_self_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :

a • s + b • interior s ⊆ interior s

If s is a convex set, then a • s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also convex.combo_closure_interior_subset_interior for a stronger version.

source

theorem convex.combo_interior_closure_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :

a • x + b • y ∈ interior s

source

theorem convex.combo_interior_self_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :

a • x + b • y ∈ interior s

source

theorem convex.combo_closure_interior_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :

a • x + b • y ∈ interior s

source

theorem convex.combo_self_interior_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :

a • x + b • y ∈ interior s

source

theorem convex.open_segment_interior_closure_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) :

open_segment 𝕜 x y ⊆ interior s

source

theorem convex.open_segment_interior_self_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s) :

open_segment 𝕜 x y ⊆ interior s

source

theorem convex.open_segment_closure_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) :

open_segment 𝕜 x y ⊆ interior s

source

theorem convex.open_segment_self_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) :

open_segment 𝕜 x y ⊆ interior s

source

theorem convex.add_smul_sub_mem_interior' {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ set.Ioc 0 1) :

x + t • (y - x) ∈ interior s

If x ∈ closure s and y ∈ interior s, then the segment (x, y] is included in interior s.

source

theorem convex.add_smul_sub_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ set.Ioc 0 1) :

x + t • (y - x) ∈ interior s

If x ∈ s and y ∈ interior s, then the segment (x, y] is included in interior s.

source

theorem convex.add_smul_mem_interior' {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ set.Ioc 0 1) :

x + t • y ∈ interior s

If x ∈ closure s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

source

theorem convex.add_smul_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ set.Ioc 0 1) :

x + t • y ∈ interior s

If x ∈ s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

source

@[protected]

theorem convex.interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) :

convex 𝕜 (interior s)

In a topological vector space, the interior of a convex set is convex.

source

@[protected]

theorem convex.closure {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) :

convex 𝕜 (closure s)

In a topological vector space, the closure of a convex set is convex.

source

theorem set.finite.compact_convex_hull {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : s.finite) :

is_compact (⇑(convex_hull ℝ) s)

Convex hull of a finite set is compact.

source

theorem set.finite.is_closed_convex_hull {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] [t2_space E] {s : set E} (hs : s.finite) :

is_closed (⇑(convex_hull ℝ) s)

Convex hull of a finite set is closed.

source

theorem convex.closure_subset_image_homothety_interior_of_one_lt {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :

closure s ⊆ ⇑(affine_map.homothety x t) '' interior s

If we dilate the interior of a convex set about a point in its interior by a scale t > 1, the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

source

theorem convex.closure_subset_interior_image_homothety_of_one_lt {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :

closure s ⊆ interior (⇑(affine_map.homothety x t) '' s)

If we dilate a convex set about a point in its interior by a scale t > 1, the interior of the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

source

theorem convex.subset_interior_image_homothety_of_one_lt {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :

s ⊆ interior (⇑(affine_map.homothety x t) '' s)

If we dilate a convex set about a point in its interior by a scale t > 1, the interior of the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

source

@[protected]

theorem convex.is_path_connected {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hconv : convex ℝ s) (hne : s.nonempty) :

is_path_connected s

A nonempty convex set is path connected.

source

@[protected]

theorem convex.is_connected {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (h : convex ℝ s) (hne : s.nonempty) :

is_connected s

A nonempty convex set is connected.

source

@[protected]

theorem convex.is_preconnected {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (h : convex ℝ s) :

is_preconnected s

A convex set is preconnected.

source

@[protected]

theorem topological_add_group.path_connected {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] :

path_connected_space E

Every topological vector space over ℝ is path connected.

Not an instance, because it creates enormous TC subproblems (turn on pp.all).

Normed vector space #

source

theorem convex_on_norm {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} (hs : convex ℝ s) :

convex_on ℝ s has_norm.norm

The norm on a real normed space is convex on any convex set. See also seminorm.convex_on and convex_on_univ_norm.

source

theorem convex_on_univ_norm {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] :

convex_on ℝ set.univ has_norm.norm

The norm on a real normed space is convex on the whole space. See also seminorm.convex_on and convex_on_norm.

source

theorem convex_on_dist {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} (z : E) (hs : convex ℝ s) :

convex_on ℝ s (λ (z' : E), has_dist.dist z' z)

source

theorem convex_on_univ_dist {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (z : E) :

convex_on ℝ set.univ (λ (z' : E), has_dist.dist z' z)

source

theorem convex_ball {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (a : E) (r : ℝ) :

convex ℝ (metric.ball a r)

source

theorem convex_closed_ball {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (a : E) (r : ℝ) :

convex ℝ (metric.closed_ball a r)

source

theorem convex.thickening {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} (hs : convex ℝ s) (δ : ℝ) :

convex ℝ (metric.thickening δ s)

source

theorem convex.cthickening {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} (hs : convex ℝ s) (δ : ℝ) :

convex ℝ (metric.cthickening δ s)

source

theorem disjoint.exists_open_convexes {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s t : set E} (disj : disjoint s t) (hs₁ : convex ℝ s) (hs₂ : is_compact s) (ht₁ : convex ℝ t) (ht₂ : is_closed t) :

∃ (u v : set E), is_open u ∧ is_open v ∧ convex ℝ u ∧ convex ℝ v ∧ s ⊆ u ∧ t ⊆ v ∧ disjoint u v

If s, t are disjoint convex sets, s is compact and t is closed then we can find open disjoint convex sets containing them.

source

theorem convex_hull_exists_dist_ge {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} {x : E} (hx : x ∈ ⇑(convex_hull ℝ) s) (y : E) :

∃ (x' : E) (H : x' ∈ s), has_dist.dist x y ≤ has_dist.dist x' y

Given a point x in the convex hull of s and a point y, there exists a point of s at distance at least dist x y from y.

source

theorem convex_hull_exists_dist_ge2 {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s t : set E} {x y : E} (hx : x ∈ ⇑(convex_hull ℝ) s) (hy : y ∈ ⇑(convex_hull ℝ) t) :

∃ (x' : E) (H : x' ∈ s) (y' : E) (H : y' ∈ t), has_dist.dist x y ≤ has_dist.dist x' y'

Given a point x in the convex hull of s and a point y in the convex hull of t, there exist points x' ∈ s and y' ∈ t at distance at least dist x y.

source

@[simp]

theorem convex_hull_ediam {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (s : set E) :

emetric.diam (⇑(convex_hull ℝ) s) = emetric.diam s

Emetric diameter of the convex hull of a set s equals the emetric diameter of `s.

source

@[simp]

theorem convex_hull_diam {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (s : set E) :

metric.diam (⇑(convex_hull ℝ) s) = metric.diam s

Diameter of the convex hull of a set s equals the emetric diameter of `s.

source

@[simp]

theorem bounded_convex_hull {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E} :

metric.bounded (⇑(convex_hull ℝ) s) ↔ metric.bounded s

Convex hull of s is bounded if and only if s is bounded.

source

@[protected, instance]

def normed_space.path_connected {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] :

path_connected_space E

source

@[protected, instance]

def normed_space.loc_path_connected {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] :

loc_path_connected_space E

source

theorem dist_add_dist_of_mem_segment {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {x y z : E} (h : y ∈ segment ℝ x z) :

has_dist.dist x y + has_dist.dist y z = has_dist.dist x z