mathlib3 documentation

analysis.convex.star

Star-convex sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files defines star-convex sets (aka star domains, star-shaped set, radially convex set).

A set is star-convex at x if every segment from x to a point in the set is contained in the set.

This is the prototypical example of a contractible set in homotopy theory (by scaling every point towards x), but has wider uses.

Note that this has nothing to do with star rings, has_star and co.

Main declarations #

Implementation notes #

Instead of saying that a set is star-convex, we say a set is star-convex at a point. This has the advantage of allowing us to talk about convexity as being "everywhere star-convexity" and of making the union of star-convex sets be star-convex.

Incidentally, this choice means we don't need to assume a set is nonempty for it to be star-convex. Concretely, the empty set is star-convex at every point.

TODO #

Balanced sets are star-convex.

The closure of a star-convex set is star-convex.

Star-convex sets are contractible.

A nonempty open star-convex set in ℝ^n is diffeomorphic to the entire space.

def star_convex (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x : E) (s : set E) :
Prop

Star-convexity of sets. s is star-convex at x if every segment from x to a point in s is contained in s.

Equations
theorem star_convex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {s : set E} :
star_convex 𝕜 x s ⦃y : E⦄, y s segment 𝕜 x y s
theorem star_convex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {s : set E} (h : star_convex 𝕜 x s) {y : E} (hy : y s) :
segment 𝕜 x y s
theorem star_convex.open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {s : set E} (h : star_convex 𝕜 x s) {y : E} (hy : y s) :
open_segment 𝕜 x y s
theorem star_convex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {s : set E} :
star_convex 𝕜 x s ⦃a b : 𝕜⦄, 0 a 0 b a + b = 1 a {x} + b s s

Alternative definition of star-convexity, in terms of pointwise set operations.

theorem star_convex_empty {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x : E) :
theorem star_convex_univ {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] (x : E) :
theorem star_convex.inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {s t : set E} (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 x t) :
star_convex 𝕜 x (s t)
theorem star_convex_sInter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {S : set (set E)} (h : (s : set E), s S star_convex 𝕜 x s) :
star_convex 𝕜 x (⋂₀ S)
theorem star_convex_Inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {ι : Sort u_3} {s : ι set E} (h : (i : ι), star_convex 𝕜 x (s i)) :
star_convex 𝕜 x ( (i : ι), s i)
theorem star_convex.union {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {s t : set E} (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 x t) :
star_convex 𝕜 x (s t)
theorem star_convex_Union {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {ι : Sort u_3} {s : ι set E} (hs : (i : ι), star_convex 𝕜 x (s i)) :
star_convex 𝕜 x ( (i : ι), s i)
theorem star_convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_smul 𝕜 E] {x : E} {S : set (set E)} (hS : (s : set E), s S star_convex 𝕜 x s) :
star_convex 𝕜 x (⋃₀ S)
theorem star_convex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [has_smul 𝕜 E] [has_smul 𝕜 F] {x : E} {y : F} {s : set E} {t : set F} (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 y t) :
star_convex 𝕜 (x, y) (s ×ˢ t)
theorem star_convex_pi {𝕜 : Type u_1} [ordered_semiring 𝕜] {ι : Type u_2} {E : ι Type u_3} [Π (i : ι), add_comm_monoid (E i)] [Π (i : ι), has_smul 𝕜 (E i)] {x : Π (i : ι), E i} {s : set ι} {t : Π (i : ι), set (E i)} (ht : ⦃i : ι⦄, i s star_convex 𝕜 (x i) (t i)) :
star_convex 𝕜 x (s.pi t)
theorem star_convex.mem {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 x s) (h : s.nonempty) :
x s
theorem star_convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hx : x s) :
star_convex 𝕜 x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a x + b y s
theorem star_convex_iff_forall_ne_pos {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hx : x s) :
star_convex 𝕜 x s ⦃y : E⦄, y s x y ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a x + b y s
theorem star_convex_iff_open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hx : x s) :
star_convex 𝕜 x s ⦃y : E⦄, y s open_segment 𝕜 x y s
theorem star_convex_singleton {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (x : E) :
star_convex 𝕜 x {x}
theorem star_convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {x : E} {s : set E} (hs : star_convex 𝕜 x s) (f : E →ₗ[𝕜] F) :
star_convex 𝕜 (f x) (f '' s)
theorem star_convex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {x : E} {s : set E} (hs : star_convex 𝕜 x s) {f : E F} (hf : is_linear_map 𝕜 f) :
star_convex 𝕜 (f x) (f '' s)
theorem star_convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {x : E} {s : set F} (f : E →ₗ[𝕜] F) (hs : star_convex 𝕜 (f x) s) :
star_convex 𝕜 x (f ⁻¹' s)
theorem star_convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {x : E} {s : set F} {f : E F} (hs : star_convex 𝕜 (f x) s) (hf : is_linear_map 𝕜 f) :
star_convex 𝕜 x (f ⁻¹' s)
theorem star_convex.add {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x y : E} {s t : set E} (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 y t) :
star_convex 𝕜 (x + y) (s + t)
theorem star_convex.add_left {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 x s) (z : E) :
star_convex 𝕜 (z + x) ((λ (x : E), z + x) '' s)
theorem star_convex.add_right {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 x s) (z : E) :
star_convex 𝕜 (x + z) ((λ (x : E), x + z) '' s)
theorem star_convex.preimage_add_right {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x z : E} {s : set E} (hs : star_convex 𝕜 (z + x) s) :
star_convex 𝕜 x ((λ (x : E), z + x) ⁻¹' s)

The translation of a star-convex set is also star-convex.

theorem star_convex.preimage_add_left {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x z : E} {s : set E} (hs : star_convex 𝕜 (x + z) s) :
star_convex 𝕜 x ((λ (x : E), x + z) ⁻¹' s)

The translation of a star-convex set is also star-convex.

theorem star_convex.sub' {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {x y : E} {s : set (E × E)} (hs : star_convex 𝕜 (x, y) s) :
star_convex 𝕜 (x - y) ((λ (x : E × E), x.fst - x.snd) '' s)
theorem star_convex.smul {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 x s) (c : 𝕜) :
star_convex 𝕜 (c x) (c s)
theorem star_convex.preimage_smul {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} {c : 𝕜} (hs : star_convex 𝕜 (c x) s) :
star_convex 𝕜 x ((λ (z : E), c z) ⁻¹' s)
theorem star_convex.affinity {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 x s) (z : E) (c : 𝕜) :
star_convex 𝕜 (z + c x) ((λ (x : E), z + c x) '' s)
theorem star_convex_zero_iff {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_monoid E] [smul_with_zero 𝕜 E] {s : set E} :
star_convex 𝕜 0 s ⦃x : E⦄, x s ⦃a : 𝕜⦄, 0 a a 1 a x s
theorem star_convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {x y : E} {s : set E} (hs : star_convex 𝕜 x s) (hy : x + y s) {t : 𝕜} (ht₀ : 0 t) (ht₁ : t 1) :
x + t y s
theorem star_convex.smul_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 0 s) (hx : x s) {t : 𝕜} (ht₀ : 0 t) (ht₁ : t 1) :
t x s
theorem star_convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {x y : E} {s : set E} (hs : star_convex 𝕜 x s) (hy : y s) {t : 𝕜} (ht₀ : 0 t) (ht₁ : t 1) :
x + t (y - x) s
theorem star_convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {x : E} (f : E →ᵃ[𝕜] F) {s : set F} (hs : star_convex 𝕜 (f x) s) :
star_convex 𝕜 x (f ⁻¹' s)

The preimage of a star-convex set under an affine map is star-convex.

theorem star_convex.affine_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {x : E} (f : E →ᵃ[𝕜] F) {s : set E} (hs : star_convex 𝕜 x s) :
star_convex 𝕜 (f x) (f '' s)

The image of a star-convex set under an affine map is star-convex.

theorem star_convex.neg {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 x s) :
star_convex 𝕜 (-x) (-s)
theorem star_convex.sub {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {x y : E} {s t : set E} (hs : star_convex 𝕜 x s) (ht : star_convex 𝕜 y t) :
star_convex 𝕜 (x - y) (s - t)
theorem star_convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {x : E} {s : set E} :
star_convex 𝕜 x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 a 0 b 0 < a + b (a / (a + b)) x + (b / (a + b)) y s

Alternative definition of star-convexity, using division.

theorem star_convex.mem_smul {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {x : E} {s : set E} (hs : star_convex 𝕜 0 s) (hx : x s) {t : 𝕜} (ht : 1 t) :
x t s

Star-convex sets in an ordered space #

Relates star_convex and set.ord_connected.

theorem set.ord_connected.star_convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {x : E} {s : set E} (hs : s.ord_connected) (hx : x s) (h : (y : E), y s x y y x) :
star_convex 𝕜 x s
theorem star_convex_iff_ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x : 𝕜} {s : set 𝕜} (hx : x s) :
theorem star_convex.ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x : 𝕜} {s : set 𝕜} (hx : x s) :

Alias of the forward direction of star_convex_iff_ord_connected.