Convex sets and functions in vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In a 𝕜-vector space, we define the following objects and properties.
convex 𝕜 s: A setsis convex if for any two pointsx y ∈ sit includessegment 𝕜 x y.std_simplex 𝕜 ι: The standard simplex inι → 𝕜(currently requiresfintype ι). It is the intersection of the positive quadrant with the hyperplanes.sum = 1.
We also provide various equivalent versions of the definitions above, prove that some specific sets are convex.
TODO #
Generalize all this file to affine spaces.
Convexity of sets #
def
convex
(𝕜 : Type u_1)
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
(s : set E) :
Prop
Convexity of sets.
theorem
convex.star_convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{s : set E}
{x : E}
(hs : convex 𝕜 s)
(hx : x ∈ s) :
star_convex 𝕜 x s
theorem
convex.segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{s : set E}
(h : convex 𝕜 s)
{x y : E}
(hx : x ∈ s)
(hy : y ∈ s) :
theorem
convex.open_segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{s : set E}
(h : convex 𝕜 s)
{x y : E}
(hx : x ∈ s)
(hy : y ∈ s) :
open_segment 𝕜 x y ⊆ s
theorem
convex_empty
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E] :
theorem
convex_univ
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E] :
theorem
convex.inter
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{s t : set E}
(hs : convex 𝕜 s)
(ht : convex 𝕜 t) :
theorem
convex_Inter
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{ι : Sort u_3}
{s : ι → set E}
(h : ∀ (i : ι), convex 𝕜 (s i)) :
theorem
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]
{s : set E}
{t : set F}
(hs : convex 𝕜 s)
(ht : convex 𝕜 t) :
theorem
directed.convex_Union
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{ι : Sort u_3}
{s : ι → set E}
(hdir : directed has_subset.subset s)
(hc : ∀ ⦃i : ι⦄, convex 𝕜 (s i)) :
theorem
directed_on.convex_sUnion
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{c : set (set E)}
(hdir : directed_on has_subset.subset c)
(hc : ∀ ⦃A : set E⦄, A ∈ c → convex 𝕜 A) :
theorem
convex_iff_open_segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E} :
theorem
convex.star_convex_iff
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
{x : E}
(hs : convex 𝕜 s)
(h : s.nonempty) :
star_convex 𝕜 x s ↔ x ∈ s
@[protected]
theorem
set.subsingleton.convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(h : s.subsingleton) :
convex 𝕜 s
theorem
convex_singleton
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
(c : E) :
convex 𝕜 {c}
theorem
convex_zero
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E] :
convex 𝕜 0
theorem
convex_segment
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
(x y : E) :
theorem
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]
{s : set E}
(hs : convex 𝕜 s)
(f : E →ₗ[𝕜] F) :
theorem
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]
{s : set E}
(hs : convex 𝕜 s)
{f : E → F}
(hf : is_linear_map 𝕜 f) :
theorem
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]
{s : set F}
(hs : convex 𝕜 s)
(f : E →ₗ[𝕜] F) :
theorem
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]
{s : set F}
(hs : convex 𝕜 s)
{f : E → F}
(hf : is_linear_map 𝕜 f) :
theorem
convex.add
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s t : set E}
(hs : convex 𝕜 s)
(ht : convex 𝕜 t) :
def
convex_add_submonoid
(𝕜 : Type u_1)
(E : Type u_2)
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E] :
add_submonoid (set E)
The convex sets form an additive submonoid under pointwise addition.
@[simp, norm_cast]
theorem
coe_convex_add_submonoid
(𝕜 : Type u_1)
(E : Type u_2)
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E] :
↑(convex_add_submonoid 𝕜 E) = {s : set E | convex 𝕜 s}
@[simp]
theorem
mem_convex_add_submonoid
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E} :
s ∈ convex_add_submonoid 𝕜 E ↔ convex 𝕜 s
theorem
convex.vadd
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(z : E) :
theorem
convex.translate
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(z : E) :
theorem
convex.translate_preimage_right
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(z : E) :
The translation of a convex set is also convex.
theorem
convex.translate_preimage_left
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(z : E) :
The translation of a convex set is also convex.
theorem
convex_Iic
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r : β) :
theorem
convex_Ici
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r : β) :
theorem
convex_Icc
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r s : β) :
theorem
convex_halfspace_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
{f : E → β}
(h : is_linear_map 𝕜 f)
(r : β) :
theorem
convex_halfspace_ge
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
{f : E → β}
(h : is_linear_map 𝕜 f)
(r : β) :
theorem
convex_hyperplane
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
{f : E → β}
(h : is_linear_map 𝕜 f)
(r : β) :
theorem
convex_Iio
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r : β) :
theorem
convex_Ioi
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r : β) :
theorem
convex_Ioo
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r s : β) :
theorem
convex_Ico
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r s : β) :
theorem
convex_Ioc
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r s : β) :
theorem
convex_halfspace_lt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
{f : E → β}
(h : is_linear_map 𝕜 f)
(r : β) :
theorem
convex_halfspace_gt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[ordered_cancel_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
{f : E → β}
(h : is_linear_map 𝕜 f)
(r : β) :
theorem
convex_uIcc
{𝕜 : Type u_1}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid β]
[module 𝕜 β]
[ordered_smul 𝕜 β]
(r s : β) :
theorem
monotone_on.convex_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
monotone_on.convex_lt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
monotone_on.convex_ge
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
monotone_on.convex_gt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
antitone_on.convex_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
antitone_on.convex_lt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
antitone_on.convex_ge
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
antitone_on.convex_gt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s)
(r : β) :
theorem
monotone.convex_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f)
(r : β) :
theorem
monotone.convex_lt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f)
(r : β) :
theorem
monotone.convex_ge
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f)
(r : β) :
theorem
monotone.convex_gt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f)
(r : β) :
theorem
antitone.convex_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f)
(r : β) :
theorem
antitone.convex_lt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f)
(r : β) :
theorem
antitone.convex_ge
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f)
(r : β) :
theorem
antitone.convex_gt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f)
(r : β) :
theorem
convex.smul
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(c : 𝕜) :
theorem
convex.smul_preimage
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(c : 𝕜) :
theorem
convex.affinity
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
(z : E)
(c : 𝕜) :
theorem
convex_open_segment
{𝕜 : Type u_1}
{E : Type u_2}
[strict_ordered_comm_semiring 𝕜]
[add_comm_group E]
[module 𝕜 E]
(a b : E) :
convex 𝕜 (open_segment 𝕜 a b)
theorem
convex.smul_mem_of_zero_mem
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s)
{x : E}
(zero_mem : 0 ∈ s)
(hx : x ∈ s)
{t : 𝕜}
(ht : t ∈ set.Icc 0 1) :
theorem
affine_subspace.convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
(Q : affine_subspace 𝕜 E) :
Affine subspaces are convex.
theorem
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]
(f : E →ᵃ[𝕜] F)
{s : set F}
(hs : convex 𝕜 s) :
The preimage of a convex set under an affine map is convex.
theorem
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]
{s : set E}
(f : E →ᵃ[𝕜] F)
(hs : convex 𝕜 s) :
The image of a convex set under an affine map is convex.
theorem
convex.neg
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : convex 𝕜 s) :
theorem
convex.sub
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t : set E}
(hs : convex 𝕜 s)
(ht : convex 𝕜 t) :
theorem
convex_iff_div
{𝕜 : Type u_1}
{E : Type u_2}
[linear_ordered_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E} :
Alternative definition of set convexity, using division.
theorem
convex.mem_smul_of_zero_mem
{𝕜 : Type u_1}
{E : Type u_2}
[linear_ordered_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(h : convex 𝕜 s)
{x : E}
(zero_mem : 0 ∈ s)
(hx : x ∈ s)
{t : 𝕜}
(ht : 1 ≤ t) :
theorem
set.ord_connected.convex_of_chain
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[ordered_add_comm_monoid E]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
(hs : s.ord_connected)
(h : is_chain has_le.le s) :
convex 𝕜 s
theorem
set.ord_connected.convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
(hs : s.ord_connected) :
convex 𝕜 s
theorem
convex_iff_ord_connected
{𝕜 : Type u_1}
[linear_ordered_field 𝕜]
{s : set 𝕜} :
convex 𝕜 s ↔ s.ord_connected
theorem
convex.ord_connected
{𝕜 : Type u_1}
[linear_ordered_field 𝕜]
{s : set 𝕜} :
convex 𝕜 s → s.ord_connected
Alias of the forward direction of convex_iff_ord_connected.
Convexity of submodules/subspaces #
@[protected]
theorem
submodule.convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
(K : submodule 𝕜 E) :
@[protected]
theorem
submodule.star_convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
(K : submodule 𝕜 E) :
star_convex 𝕜 0 ↑K
Simplex #
The standard simplex in the space of functions ι → 𝕜 is the set of vectors with non-negative
coordinates with total sum 1. This is the free object in the category of convex spaces.
Equations
- std_simplex 𝕜 ι = {f : ι → 𝕜 | (∀ (x : ι), 0 ≤ f x) ∧ finset.univ.sum (λ (x : ι), f x) = 1}
theorem
convex_std_simplex
(𝕜 : Type u_1)
(ι : Type u_5)
[ordered_semiring 𝕜]
[fintype ι] :
convex 𝕜 (std_simplex 𝕜 ι)
theorem
ite_eq_mem_std_simplex
(𝕜 : Type u_1)
{ι : Type u_5}
[ordered_semiring 𝕜]
[fintype ι]
(i : ι) :
(λ (j : ι), ite (i = j) 1 0) ∈ std_simplex 𝕜 ι