mathlib3 documentation

analysis.convex.normed

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:

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

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

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)
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)
theorem convex_ball {E : Type u_2} [seminormed_add_comm_group E] [normed_space E] (a : E) (r : ) :
theorem convex.thickening {E : Type u_2} [seminormed_add_comm_group E] [normed_space E] {s : set E} (hs : convex s) (δ : ) :
theorem convex.cthickening {E : Type u_2} [seminormed_add_comm_group E] [normed_space E] {s : set E} (hs : convex s) (δ : ) :
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.

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.

@[simp]

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

@[simp]

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

@[simp]

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

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

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.