Topological and 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;
• bounded_convexHull : convex hull of a set is bounded if and only if the original set is bounded.

theorem convexOn_norm {E : Type u_2} [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.

theorem convexOn_univ_norm {E : Type u_2} [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.

theorem convexOn_dist {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (z : E) (hs : Convex ℝ s) : ConvexOn ℝ s fun (z' : E) => dist z' z

theorem convexOn_univ_dist {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (z : E) : ConvexOn ℝ Set.univ fun (z' : E) => dist z' z

theorem convex_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : E) (r : ℝ) : Convex ℝ (Metric.ball a r)

theorem convex_closedBall {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : E) (r : ℝ) : Convex ℝ (Metric.closedBall a r)

theorem Convex.thickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (δ : ℝ) : Convex ℝ (Metric.thickening δ s)

theorem Convex.cthickening {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (δ : ℝ) : Convex ℝ (Metric.cthickening δ s)

theorem convexHull_exists_dist_ge {E : Type u_2} [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.

theorem convexHull_exists_dist_ge2 {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {t : Set E} {x : E} {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.

@[simp]

theorem convexHull_ediam {E : Type u_2} [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.

@[simp]

theorem convexHull_diam {E : Type u_2} [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.

@[simp]

theorem isBounded_convexHull {E : Type u_2} [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.

@[instance 100]

instance NormedSpace.instPathConnectedSpace {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : PathConnectedSpace E

Equations

• ⋯ = ⋯

@[instance 100]

instance NormedSpace.instLocPathConnectedSpace {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : LocPathConnectedSpace E

Equations

• ⋯ = ⋯

theorem Wbtw.dist_add_dist {E : Type u_2} {P : Type u_3} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PseudoMetricSpace P] [NormedAddTorsor E P] {x : P} {y : P} {z : P} (h : Wbtw ℝ x y z) : dist x y + dist y z = dist x z

theorem dist_add_dist_of_mem_segment {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {y : E} {z : E} (h : y ∈ segment ℝ x z) : dist x y + dist y z = dist x z

theorem isConnected_setOf_sameRay {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : IsConnected {y : E | SameRay ℝ x y}

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

theorem isConnected_setOf_sameRay_and_ne_zero {E : Type u_2} [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.

theorem exists_mem_interior_convexHull_affineBasis {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E} (hs : s ∈ nhds x) : ∃ (b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E), x ∈ interior ((convexHull ℝ) (Set.range ⇑b)) ∧ (convexHull ℝ) (Set.range ⇑b) ⊆ s

We can intercalate a simplex between a point and one of its neighborhoods.