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)
:
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
Instances For
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)
:
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)
:
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)
:
@[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]
:
@[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, ⋯⟩) ⋯ ⋯
Instances For
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)
:
@[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)
:
@[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)
:
@[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)
:
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.