Documentation

Mathlib.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, 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 StarConvex (๐•œ : Type u_1) {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] (x : E) (s : Set E) :

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

Instances For
    theorem starConvex_iff_segment_subset {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {s : Set E} :
    StarConvex ๐•œ x s โ†” โˆ€ โฆƒy : Eโฆ„, y โˆˆ s โ†’ segment ๐•œ x y โŠ† s
    theorem StarConvex.segment_subset {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {s : Set E} (h : StarConvex ๐•œ x s) {y : E} (hy : y โˆˆ s) :
    segment ๐•œ x y โŠ† s
    theorem StarConvex.openSegment_subset {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {s : Set E} (h : StarConvex ๐•œ x s) {y : E} (hy : y โˆˆ s) :
    openSegment ๐•œ x y โŠ† s
    theorem starConvex_iff_pointwise_add_subset {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {s : Set E} :
    StarConvex ๐•œ 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 starConvex_empty {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] (x : E) :
    StarConvex ๐•œ x โˆ…
    theorem starConvex_univ {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] (x : E) :
    StarConvex ๐•œ x Set.univ
    theorem StarConvex.inter {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {s : Set E} {t : Set E} (hs : StarConvex ๐•œ x s) (ht : StarConvex ๐•œ x t) :
    StarConvex ๐•œ x (s โˆฉ t)
    theorem starConvex_sInter {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {S : Set (Set E)} (h : โˆ€ (s : Set E), s โˆˆ S โ†’ StarConvex ๐•œ x s) :
    StarConvex ๐•œ x (โ‹‚โ‚€ S)
    theorem starConvex_iInter {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {ฮน : Sort u_4} {s : ฮน โ†’ Set E} (h : โˆ€ (i : ฮน), StarConvex ๐•œ x (s i)) :
    StarConvex ๐•œ x (โ‹‚ (i : ฮน), s i)
    theorem StarConvex.union {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {s : Set E} {t : Set E} (hs : StarConvex ๐•œ x s) (ht : StarConvex ๐•œ x t) :
    StarConvex ๐•œ x (s โˆช t)
    theorem starConvex_iUnion {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {ฮน : Sort u_4} {s : ฮน โ†’ Set E} (hs : โˆ€ (i : ฮน), StarConvex ๐•œ x (s i)) :
    StarConvex ๐•œ x (โ‹ƒ (i : ฮน), s i)
    theorem starConvex_sUnion {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [SMul ๐•œ E] {x : E} {S : Set (Set E)} (hS : โˆ€ (s : Set E), s โˆˆ S โ†’ StarConvex ๐•œ x s) :
    StarConvex ๐•œ x (โ‹ƒโ‚€ S)
    theorem StarConvex.prod {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring ๐•œ] [AddCommMonoid E] [AddCommMonoid F] [SMul ๐•œ E] [SMul ๐•œ F] {x : E} {y : F} {s : Set E} {t : Set F} (hs : StarConvex ๐•œ x s) (ht : StarConvex ๐•œ y t) :
    StarConvex ๐•œ (x, y) (s ร—หข t)
    theorem starConvex_pi {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {ฮน : Type u_4} {E : ฮน โ†’ Type u_5} [(i : ฮน) โ†’ AddCommMonoid (E i)] [(i : ฮน) โ†’ SMul ๐•œ (E i)] {x : (i : ฮน) โ†’ E i} {s : Set ฮน} {t : (i : ฮน) โ†’ Set (E i)} (ht : โˆ€ โฆƒi : ฮนโฆ„, i โˆˆ s โ†’ StarConvex ๐•œ (x i) (t i)) :
    StarConvex ๐•œ x (Set.pi s t)
    theorem StarConvex.mem {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) (h : Set.Nonempty s) :
    theorem starConvex_iff_forall_pos {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hx : x โˆˆ s) :
    StarConvex ๐•œ x s โ†” โˆ€ โฆƒy : Eโฆ„, y โˆˆ s โ†’ โˆ€ โฆƒa b : ๐•œโฆ„, 0 < a โ†’ 0 < b โ†’ a + b = 1 โ†’ a โ€ข x + b โ€ข y โˆˆ s
    theorem starConvex_iff_forall_ne_pos {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hx : x โˆˆ s) :
    StarConvex ๐•œ x s โ†” โˆ€ โฆƒy : Eโฆ„, y โˆˆ s โ†’ x โ‰  y โ†’ โˆ€ โฆƒa b : ๐•œโฆ„, 0 < a โ†’ 0 < b โ†’ a + b = 1 โ†’ a โ€ข x + b โ€ข y โˆˆ s
    theorem starConvex_iff_openSegment_subset {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hx : x โˆˆ s) :
    StarConvex ๐•œ x s โ†” โˆ€ โฆƒy : Eโฆ„, y โˆˆ s โ†’ openSegment ๐•œ x y โŠ† s
    theorem starConvex_singleton {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] (x : E) :
    StarConvex ๐•œ x {x}
    theorem StarConvex.linear_image {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring ๐•œ] [AddCommMonoid E] [AddCommMonoid F] [Module ๐•œ E] [Module ๐•œ F] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) (f : E โ†’โ‚—[๐•œ] F) :
    StarConvex ๐•œ (โ†‘f x) (โ†‘f '' s)
    theorem StarConvex.is_linear_image {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring ๐•œ] [AddCommMonoid E] [AddCommMonoid F] [Module ๐•œ E] [Module ๐•œ F] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) {f : E โ†’ F} (hf : IsLinearMap ๐•œ f) :
    StarConvex ๐•œ (f x) (f '' s)
    theorem StarConvex.linear_preimage {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring ๐•œ] [AddCommMonoid E] [AddCommMonoid F] [Module ๐•œ E] [Module ๐•œ F] {x : E} {s : Set F} (f : E โ†’โ‚—[๐•œ] F) (hs : StarConvex ๐•œ (โ†‘f x) s) :
    StarConvex ๐•œ x (โ†‘f โปยน' s)
    theorem StarConvex.is_linear_preimage {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring ๐•œ] [AddCommMonoid E] [AddCommMonoid F] [Module ๐•œ E] [Module ๐•œ F] {x : E} {s : Set F} {f : E โ†’ F} (hs : StarConvex ๐•œ (f x) s) (hf : IsLinearMap ๐•œ f) :
    StarConvex ๐•œ x (f โปยน' s)
    theorem StarConvex.add {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {y : E} {s : Set E} {t : Set E} (hs : StarConvex ๐•œ x s) (ht : StarConvex ๐•œ y t) :
    StarConvex ๐•œ (x + y) (s + t)
    theorem StarConvex.add_left {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) (z : E) :
    StarConvex ๐•œ (z + x) ((fun x => z + x) '' s)
    theorem StarConvex.add_right {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) (z : E) :
    StarConvex ๐•œ (x + z) ((fun x => x + z) '' s)
    theorem StarConvex.preimage_add_right {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {z : E} {s : Set E} (hs : StarConvex ๐•œ (z + x) s) :
    StarConvex ๐•œ x ((fun x => z + x) โปยน' s)

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

    theorem StarConvex.preimage_add_left {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {z : E} {s : Set E} (hs : StarConvex ๐•œ (x + z) s) :
    StarConvex ๐•œ x ((fun x => x + z) โปยน' s)

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

    theorem StarConvex.sub' {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {y : E} {s : Set (E ร— E)} (hs : StarConvex ๐•œ (x, y) s) :
    StarConvex ๐•œ (x - y) ((fun x => x.fst - x.snd) '' s)
    theorem StarConvex.smul {๐•œ : Type u_1} {E : Type u_2} [OrderedCommSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) (c : ๐•œ) :
    StarConvex ๐•œ (c โ€ข x) (c โ€ข s)
    theorem StarConvex.preimage_smul {๐•œ : Type u_1} {E : Type u_2} [OrderedCommSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} {c : ๐•œ} (hs : StarConvex ๐•œ (c โ€ข x) s) :
    StarConvex ๐•œ x ((fun z => c โ€ข z) โปยน' s)
    theorem StarConvex.affinity {๐•œ : Type u_1} {E : Type u_2} [OrderedCommSemiring ๐•œ] [AddCommMonoid E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) (z : E) (c : ๐•œ) :
    StarConvex ๐•œ (z + c โ€ข x) ((fun x => z + c โ€ข x) '' s)
    theorem starConvex_zero_iff {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommMonoid E] [SMulWithZero ๐•œ E] {s : Set E} :
    StarConvex ๐•œ 0 s โ†” โˆ€ โฆƒx : Eโฆ„, x โˆˆ s โ†’ โˆ€ โฆƒa : ๐•œโฆ„, 0 โ‰ค a โ†’ a โ‰ค 1 โ†’ a โ€ข x โˆˆ s
    theorem StarConvex.add_smul_mem {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {y : E} {s : Set E} (hs : StarConvex ๐•œ x s) (hy : x + y โˆˆ s) {t : ๐•œ} (htโ‚€ : 0 โ‰ค t) (htโ‚ : t โ‰ค 1) :
    theorem StarConvex.smul_mem {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ 0 s) (hx : x โˆˆ s) {t : ๐•œ} (htโ‚€ : 0 โ‰ค t) (htโ‚ : t โ‰ค 1) :
    theorem StarConvex.add_smul_sub_mem {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {y : E} {s : Set E} (hs : StarConvex ๐•œ x s) (hy : y โˆˆ s) {t : ๐•œ} (htโ‚€ : 0 โ‰ค t) (htโ‚ : t โ‰ค 1) :
    x + t โ€ข (y - x) โˆˆ s
    theorem StarConvex.affine_preimage {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedRing ๐•œ] [AddCommGroup E] [AddCommGroup F] [Module ๐•œ E] [Module ๐•œ F] {x : E} (f : E โ†’แตƒ[๐•œ] F) {s : Set F} (hs : StarConvex ๐•œ (โ†‘f x) s) :
    StarConvex ๐•œ x (โ†‘f โปยน' s)

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

    theorem StarConvex.affine_image {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedRing ๐•œ] [AddCommGroup E] [AddCommGroup F] [Module ๐•œ E] [Module ๐•œ F] {x : E} (f : E โ†’แตƒ[๐•œ] F) {s : Set E} (hs : StarConvex ๐•œ x s) :
    StarConvex ๐•œ (โ†‘f x) (โ†‘f '' s)

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

    theorem StarConvex.neg {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ x s) :
    StarConvex ๐•œ (-x) (-s)
    theorem StarConvex.sub {๐•œ : Type u_1} {E : Type u_2} [OrderedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {y : E} {s : Set E} {t : Set E} (hs : StarConvex ๐•œ x s) (ht : StarConvex ๐•œ y t) :
    StarConvex ๐•œ (x - y) (s - t)
    theorem starConvex_iff_div {๐•œ : Type u_1} {E : Type u_2} [LinearOrderedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {s : Set E} :
    StarConvex ๐•œ 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 StarConvex.mem_smul {๐•œ : Type u_1} {E : Type u_2} [LinearOrderedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {x : E} {s : Set E} (hs : StarConvex ๐•œ 0 s) (hx : x โˆˆ s) {t : ๐•œ} (ht : 1 โ‰ค t) :

    Star-convex sets in an ordered space #

    Relates starConvex and Set.ordConnected.

    theorem Set.OrdConnected.starConvex {๐•œ : Type u_1} {E : Type u_2} [OrderedSemiring ๐•œ] [OrderedAddCommMonoid E] [Module ๐•œ E] [OrderedSMul ๐•œ E] {x : E} {s : Set E} (hs : Set.OrdConnected s) (hx : x โˆˆ s) (h : โˆ€ (y : E), y โˆˆ s โ†’ x โ‰ค y โˆจ y โ‰ค x) :
    StarConvex ๐•œ x s
    theorem starConvex_iff_ordConnected {๐•œ : Type u_1} [LinearOrderedField ๐•œ] {x : ๐•œ} {s : Set ๐•œ} (hx : x โˆˆ s) :
    theorem StarConvex.ordConnected {๐•œ : Type u_1} [LinearOrderedField ๐•œ] {x : ๐•œ} {s : Set ๐•œ} (hx : x โˆˆ s) :
    StarConvex ๐•œ x s โ†’ Set.OrdConnected s

    Alias of the forward direction of starConvex_iff_ordConnected.