# Metric properties of convex sets in normed spaces #

We prove the following facts:

- `convexOn_norm`, `convexOn_dist` : norm and distance to a fixed point is convex on any convex set;
- `convexOn_univ_norm`, `convexOn_univ_dist` : norm and distance to a fixed point is convex on the whole space;
- `convexHull_ediam`, `convexHull_diam` : convex hull of a set has the same (e)metric diameter as the original set;
- `isBounded_convexHull` : convex hull of a set is bounded if and only if the original set is bounded.

source
theorem convexOn_norm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) :
ConvexOn ℝ s norm

The norm on a real normed space is convex on any convex set. See also `Seminorm.convexOn` and `convexOn_univ_norm`.

source
theorem convexOn_univ_norm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] :
ConvexOn ℝ Set.univ norm

The norm on a real normed space is convex on the whole space. See also `Seminorm.convexOn` and `convexOn_norm`.

source
theorem convexOn_dist {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (z : E) (hs : Convex ℝ s) :
ConvexOn ℝ s fun (z' : E) => dist z' z
source
theorem convexOn_univ_dist {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (z : E) :
ConvexOn ℝ Set.univ fun (z' : E) => dist z' z
source
theorem convex_ball {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : E) (r : ℝ) :
Convex ℝ (Metric.ball a r)
source
theorem convex_closedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : E) (r : ℝ) :
Convex ℝ (Metric.closedBall a r)
source
theorem convexHull_sphere_eq_closedBall {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [Nontrivial F] (x : F) {r : ℝ} (hr : 0 ≤ r) :
(convexHull ℝ) (Metric.sphere x r) = Metric.closedBall x r
source
theorem convexHull_exists_dist_ge {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x : E} (hx : x ∈ (convexHull ℝ) s) (y : E) :
∃ x' ∈ s, dist x y ≤ 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.thickening {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (δ : ℝ) :
Convex ℝ (Metric.thickening δ s)
source
theorem Convex.cthickening {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (δ : ℝ) :
Convex ℝ (Metric.cthickening δ s)
source
theorem convexHull_exists_dist_ge2 {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set E} {x y : E} (hx : x ∈ (convexHull ℝ) s) (hy : y ∈ (convexHull ℝ) t) :
∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ 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 convexHull_ediam {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) :
EMetric.diam ((convexHull ℝ) s) = EMetric.diam s

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

source
@[simp]
theorem convexHull_diam {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) :
Metric.diam ((convexHull ℝ) s) = Metric.diam s

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

source
@[simp]
theorem isBounded_convexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} :
Bornology.IsBounded ((convexHull ℝ) s) ↔ Bornology.IsBounded s

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

source
@[instance 100]
instance NormedSpace.instPathConnectedSpace {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] :
PathConnectedSpace E
source
theorem isConnected_setOf_sameRay {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) :
IsConnected {y : E | SameRay ℝ x y}

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

source
theorem isConnected_setOf_sameRay_and_ne_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} (hx : x ≠ 0) :
IsConnected {y : E | SameRay ℝ x y ∧ y ≠ 0}

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

source
theorem norm_sub_le_of_mem_segment {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y z : E} (hy : y ∈ segment ℝ x z) :
‖y - x‖ ≤ ‖z - x‖
source
theorem Filter.Eventually.segment_of_prod_nhds {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {α : Type u_3} {f : Filter α} {x : E} {y z : α → E} {r : α → E → Prop} (hy : Tendsto y f (nhds x)) (hz : Tendsto z f (nhds x)) (hr : ∀ᶠ (p : α × E) in f ×ˢ nhds x, r p.1 p.2) :
∀ᶠ (χ : α) in f, ∀ v ∈ segment ℝ (y χ) (z χ), r χ v
source
theorem Filter.Eventually.segment_of_prod_nhdsWithin {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {α : Type u_3} {f : Filter α} {x : E} {y z : α → E} {r : α → E → Prop} (hy : Tendsto y f (nhds x)) (hz : Tendsto z f (nhds x)) (hr : ∀ᶠ (p : α × E) in f ×ˢ nhdsWithin x s, r p.1 p.2) (seg : ∀ᶠ (χ : α) in f, segment ℝ (y χ) (z χ) ⊆ s) :
∀ᶠ (χ : α) in f, ∀ v ∈ segment ℝ (y χ) (z χ), r χ v