mathlib documentation

analysis.convex.topology

Topological and metric properties of convex sets #

We prove the following facts:

Standard simplex #

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

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

std_simplex ℝ ι is bounded.

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

std_simplex ℝ ι is closed.

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

std_simplex ℝ ι is compact.

Topological vector space #

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

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

Convex hull of a finite set is compact.

Convex hull of a finite set is closed.

theorem convex.add_smul_sub_mem_interior {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 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.

theorem convex.add_smul_mem_interior {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 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].

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

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

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

Normed vector space #

theorem convex_on_dist {E : Type u_2} [normed_group E] [normed_space E] (z : E) (s : set E) (hs : convex s) :
convex_on s (λ (z' : E), dist z' z)
theorem convex_ball {E : Type u_2} [normed_group E] [normed_space E] (a : E) (r : ) :
theorem convex_closed_ball {E : Type u_2} [normed_group E] [normed_space E] (a : E) (r : ) :
theorem convex_hull_exists_dist_ge {E : Type u_2} [normed_group E] [normed_space E] {s : set E} {x : E} (hx : x (convex_hull ) s) (y : E) :
∃ (x' : E) (H : 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 convex_hull_exists_dist_ge2 {E : Type u_2} [normed_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), 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 convex_hull_ediam {E : Type u_2} [normed_group E] [normed_space E] (s : set E) :

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

@[simp]
theorem convex_hull_diam {E : Type u_2} [normed_group E] [normed_space E] (s : set E) :

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.

theorem convex.is_path_connected {E : Type u_2} [normed_group E] [normed_space E] {s : set E} (hconv : convex s) (hne : s.nonempty) :