Convex sets

This file defines convex sets in a convex space.

Implementation notes

To support non-field coefficients, for s to be convex we require that all finitary convex combinations of points of s lie in s, instead of merely binary ones as is customary.

Since its body is an implementation detail, the predicate IsConvexSet is unexposed.

def Convexity.IsConvexSet (R : Type u_3) {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : Set X) : Prop

A set s in a convex space is convex if all convex combinations of points in s lie themselves in s.

When the scalars form a field, this is equivalent to the definition in terms of binary combinations. See IsConvexSet.of_convexCombPair_mem.

Equations

• Convexity.IsConvexSet R s = ∀ ⦃w : Convexity.StdSimplex R X⦄, ↑w.weights.support ⊆ s → Convexity.sConvexComb w ∈ s

theorem Convexity.IsConvexSet.of_sConvexComb_mem {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} (hs : ∀ (w : StdSimplex R X), ↑w.weights.support ⊆ s → sConvexComb w ∈ s) : IsConvexSet R s

theorem Convexity.IsConvexSet.sConvexComb_mem {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {w : StdSimplex R X} {s : Set X} (hs : IsConvexSet R s) (hw : ↑w.weights.support ⊆ s) : sConvexComb w ∈ s

theorem Convexity.IsConvexSet.iConvexComb_mem {ι : Type u_1} {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} (hs : IsConvexSet R s) {w : StdSimplex R ι} {f : ι → X} (hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s) : iConvexComb w f ∈ s

theorem Convexity.IsConvexSet.convexCombPair_mem {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} {x y : X} (hs : IsConvexSet R s) (hx : x ∈ s) (hy : y ∈ s) {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : convexCombPair a b ha hb hab x y ∈ s

@[simp]

theorem Convexity.IsConvexSet.empty {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] : IsConvexSet R ∅

@[simp]

theorem Convexity.IsConvexSet.univ {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] : IsConvexSet R Set.univ

@[simp]

theorem Convexity.IsConvexSet.singleton {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {x : X} : IsConvexSet R {x}

theorem Convexity.IsConvexSet.of_subsingleton {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} (hs : s.Subsingleton) : IsConvexSet R s

theorem Convexity.IsConvexSet.inter {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : Set X} (hs : IsConvexSet R s) (ht : IsConvexSet R t) : IsConvexSet R (s ∩ t)

theorem Convexity.IsConvexSet.sInter {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {S : Set (Set X)} (hS : ∀ s ∈ S, IsConvexSet R s) : IsConvexSet R (⋂₀ S)

theorem Convexity.IsConvexSet.iInter {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {ι : Sort u_7} {s : ι → Set X} (hs : ∀ (i : ι), IsConvexSet R (s i)) : IsConvexSet R (⋂ (i : ι), s i)

theorem Convexity.IsConvexSet.iInter₂ {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {ι : Sort u_7} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set X} (h : ∀ (i : ι) (j : κ i), IsConvexSet R (s i j)) : IsConvexSet R (⋂ (i : ι), ⋂ (j : κ i), s i j)

theorem Convexity.IsConvexSet.sUnion {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {S : Set (Set X)} (hS : DirectedOn (fun (x1 x2 : Set X) => x1 ⊆ x2) S) (hS' : ∀ s ∈ S, IsConvexSet R s) : IsConvexSet R (⋃₀ S)

theorem Convexity.IsConvexSet.iUnion {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {ι : Sort u_7} {s : ι → Set X} (hs : Directed (fun (x1 x2 : Set X) => x1 ⊆ x2) s) (hs' : ∀ (i : ι), IsConvexSet R (s i)) : IsConvexSet R (⋃ (i : ι), s i)

theorem Convexity.IsConvexSet.preimage {R : Type u_3} {X : Type u_5} {Y : Type u_6} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] {f : X → Y} {s : Set Y} (hf : IsAffineMap R f) (hs : IsConvexSet R s) : IsConvexSet R (f ⁻¹' s)

theorem Convexity.IsConvexSet.image {R : Type u_3} {X : Type u_5} {Y : Type u_6} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] {f : X → Y} {s : Set X} (hf : IsAffineMap R f) (hs : IsConvexSet R s) : IsConvexSet R (f '' s)

@[implicit_reducible]

noncomputable def Convexity.ConvexSpace.subtype {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : Set X) (hs : IsConvexSet R s) : ConvexSpace R ↑s

A convex subset of a convex space is a convex space.

Equations

• Convexity.ConvexSpace.subtype s hs = Convexity.ConvexSpace.mk (fun (w : Convexity.StdSimplex R ↑s) => ⟨Convexity.iConvexComb w Subtype.val, ⋯⟩) ⋯ ⋯

theorem Convexity.isAffineMap_subtypeVal {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : Set X) (hs : IsConvexSet R s) : IsAffineMap R Subtype.val

@[simp]

theorem Convexity.subtypeVal_sConvexComb {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : Set X) (hs : IsConvexSet R s) (w : StdSimplex R ↑s) : ↑(sConvexComb w) = iConvexComb w Subtype.val

@[simp]

theorem Convexity.subtypeVal_iConvexComb {I : Type u_2} {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : Set X) (hs : IsConvexSet R s) (w : StdSimplex R I) (f : I → ↑s) : ↑(iConvexComb w f) = iConvexComb w fun (i : I) => ↑(f i)

@[simp]

theorem Convexity.subtypeVal_convexCombPair {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s : Set X) (hs : IsConvexSet R s) (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : ↑s) : ↑(convexCombPair a b ha hb hab x y) = convexCombPair a b ha hb hab ↑x ↑y

theorem Convexity.IsConvexSet.prod {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} {Y : Type u_7} [ConvexSpace R Y] {t : Set Y} (hs : IsConvexSet R s) (ht : IsConvexSet R t) : IsConvexSet R (s ×ˢ t)

theorem Convexity.IsConvexSet.pi {ι : Type u_1} {R : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : ι → Type u_7} [(i : ι) → ConvexSpace R (X i)] {s : Set ι} {t : (i : ι) → Set (X i)} (ht : ∀ i ∈ s, IsConvexSet R (t i)) : IsConvexSet R (s.pi t)

theorem Convexity.IsConvexSet.of_convexCombPair_mem {K : Type u_4} {X : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [ConvexSpace K X] {s : Set X} (hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s) : IsConvexSet K s

Convexity of a set can be checked via binary combinations if the scalars form a field.