mathlib documentation

analysis.convex.star

Star-convex sets #

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) :
star_convex π•œ x βˆ…
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) :
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) :
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) :

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

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) :
star_convex π•œ x s β†’ s.ord_connected

Alias of the forward direction of star_convex_iff_ord_connected.