mathlib documentation

analysis.convex.topology

Topological and metric properties of convex sets #

We prove the following facts:

Alias of the reverse direction of real.convex_iff_is_preconnected.

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 is_compact_std_simplex (ι : Type u_1) [fintype ι] :

std_simplex ℝ ι is compact.

Topological vector space #

theorem convex.combo_interior_closure_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) :

If s is a convex set, then a • interior s + b • closure s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also convex.combo_interior_self_subset_interior for a weaker version.

theorem convex.combo_interior_self_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) :

If s is a convex set, then a • interior s + b • s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also convex.combo_interior_closure_subset_interior for a stronger version.

theorem convex.combo_closure_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) :

If s is a convex set, then a • closure s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also convex.combo_self_interior_subset_interior for a weaker version.

theorem convex.combo_self_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {a b : 𝕜} (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) :

If s is a convex set, then a • s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also convex.combo_closure_interior_subset_interior for a stronger version.

theorem convex.combo_interior_closure_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x interior s) (hy : y closure s) {a b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) :
a x + b y interior s
theorem convex.combo_interior_self_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x interior s) (hy : y s) {a b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) :
a x + b y interior s
theorem convex.combo_closure_interior_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x closure s) (hy : y interior s) {a b : 𝕜} (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) :
a x + b y interior s
theorem convex.combo_self_interior_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x s) (hy : y interior s) {a b : 𝕜} (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) :
a x + b y interior s
theorem convex.open_segment_interior_closure_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x interior s) (hy : y closure s) :
theorem convex.open_segment_interior_self_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x interior s) (hy : y s) :
theorem convex.open_segment_closure_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x closure s) (hy : y interior s) :
theorem convex.open_segment_self_interior_subset_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x s) (hy : y interior s) :
theorem convex.add_smul_sub_mem_interior' {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x closure s) (hy : y interior s) {t : 𝕜} (ht : t set.Ioc 0 1) :
x + t (y - x) interior s

If x ∈ closure s and y ∈ interior s, then the segment (x, y] is included in interior s.

theorem convex.add_smul_sub_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_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} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x closure s) (hy : x + y interior s) {t : 𝕜} (ht : t set.Ioc 0 1) :
x + t y interior s

If x ∈ closure s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

theorem convex.add_smul_mem_interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_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].

@[protected]
theorem convex.interior {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) :
convex 𝕜 (interior s)

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

@[protected]
theorem convex.closure {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) :
convex 𝕜 (closure s)

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

@[protected]
theorem convex.strict_convex' {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) (h : (s \ interior s).pairwise (λ (x y : E), (c : 𝕜), (affine_map.line_map x y) c interior s)) :

A convex set s is strictly convex provided that for any two distinct points of s \ interior s, the line passing through these points has nonempty intersection with interior s.

@[protected]
theorem convex.strict_convex {E : Type u_2} {𝕜 : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) (h : (s \ interior s).pairwise (λ (x y : E), (segment 𝕜 x y \ frontier s).nonempty)) :

A convex set s is strictly convex provided that for any two distinct points x, y of s \ interior s, the segment with endpoints x, y has nonempty intersection with interior s.

Convex hull of a finite set is compact.

Convex hull of a finite set is closed.

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

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

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

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

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

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

@[protected]

A nonempty convex set is path connected.

@[protected]

A nonempty convex set is connected.

@[protected]

A convex set is preconnected.

@[protected]

Every topological vector space over ℝ is path connected.

Not an instance, because it creates enormous TC subproblems (turn on pp.all).

Normed vector space #

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.