Topological and metric properties of convex sets in normed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove the following facts:

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

source

theorem is_connected_set_of_same_ray {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) :

is_connected {y : E | same_ray ℝ x y}

The set of vectors in the same ray as x is connected.

source

theorem is_connected_set_of_same_ray_and_ne_zero {E : Type u_2} [seminormed_add_comm_group E] [normed_space ℝ E] {x : E} (hx : x ≠ 0) :

is_connected {y : E | same_ray ℝ x y ∧ y ≠ 0}

The set of nonzero vectors in the same ray as the nonzero vector x is connected.