Convex sets and functions in vector spaces #
In a π-vector space, we define the following objects and properties.
segment π x y: Closed segment joiningxandy.open_segment π x y: Open segment joiningxandy.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.
Notations #
We provide the following notation:
TODO #
Generalize all this file to affine spaces.
Should we rename segment and open_segment to convex.Icc and convex.Ioo? Should we also
define clopen_segment/convex.Ico/convex.Ioc?
Segment #
def
open_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
(x y : E) :
set E
Open segment in a vector space. Note that open_segment π x x = {x} instead of being β
when
the base semiring has some element between 0 and 1.
theorem
segment_symm
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
(x y : E) :
theorem
open_segment_symm
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
(x y : E) :
open_segment π x y = open_segment π y x
theorem
open_segment_subset_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
(x y : E) :
theorem
segment_subset_iff
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{x y : E}
{s : set E} :
theorem
open_segment_subset_iff
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{x y : E}
{s : set E} :
theorem
left_mem_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[mul_action_with_zero π E]
(x y : E) :
theorem
right_mem_segment
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[mul_action_with_zero π E]
(x y : E) :
theorem
segment_same
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(x : E) :
theorem
mem_open_segment_of_ne_left_right
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{x y z : E}
(hx : x β z)
(hy : y β z)
(hz : z β [x -[π] y]) :
z β open_segment π x y
theorem
open_segment_subset_iff_segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{x y : E}
{s : set E}
(hx : x β s)
(hy : y β s) :
theorem
convex.combo_self
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{a b : π}
(h : a + b = 1)
(x : E) :
@[simp]
theorem
open_segment_same
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
[nontrivial π]
[densely_ordered π]
(x : E) :
open_segment π x x = {x}
theorem
open_segment_eq_image
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
segment_eq_image'
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
open_segment_eq_image'
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
segment_eq_image_line_map
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
open_segment_eq_image_line_map
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(x y : E) :
open_segment π x y = β(affine_map.line_map x y) '' set.Ioo 0 1
@[simp]
theorem
open_segment_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]
(f : E ββ[π] F)
(a b : E) :
βf '' open_segment π a b = open_segment π (βf a) (βf b)
@[simp]
theorem
mem_open_segment_translate
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a : E)
{x b c : E} :
a + x β open_segment π (a + b) (a + c) β x β open_segment π b c
theorem
open_segment_translate_preimage
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a b c : E) :
(Ξ» (x : E), a + x) β»ΒΉ' open_segment π (a + b) (a + c) = open_segment π b c
theorem
open_segment_translate_image
(π : Type u_1)
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(a b c : E) :
(Ξ» (x : E), a + x) '' open_segment π b c = open_segment π (a + b) (a + c)
theorem
midpoint_mem_segment
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
[invertible 2]
(x y : E) :
theorem
mem_segment_sub_add
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
[invertible 2]
(x y : E) :
theorem
mem_segment_add_sub
{π : Type u_1}
{E : Type u_2}
[linear_ordered_ring π]
[add_comm_group E]
[module π E]
[invertible 2]
(x y : E) :
theorem
mem_open_segment_iff_div
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{x y z : E} :
@[simp]
theorem
left_mem_open_segment_iff
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
[no_zero_smul_divisors π E]
{x y : E} :
x β open_segment π x y β x = y
@[simp]
theorem
right_mem_open_segment_iff
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{x y : E} :
y β open_segment π x y β x = y
theorem
segment_subset_Icc
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{x y : E}
(h : x β€ y) :
theorem
open_segment_subset_Ioo
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{x y : E}
(h : x < y) :
open_segment π x y β set.Ioo x y
theorem
segment_subset_interval
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
(x y : E) :
theorem
convex.min_le_combo
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
(x y : E)
{a b : π}
(ha : 0 β€ a)
(hb : 0 β€ b)
(hab : a + b = 1) :
theorem
convex.combo_le_max
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
(x y : E)
{a b : π}
(ha : 0 β€ a)
(hb : 0 β€ b)
(hab : a + b = 1) :
@[simp]
theorem
Ioo_subset_open_segment
{π : Type u_1}
[linear_ordered_field π]
{x y : π} :
set.Ioo x y β open_segment π x y
@[simp]
theorem
open_segment_eq_Ioo
{π : Type u_1}
[linear_ordered_field π]
{x y : π}
(h : x < y) :
open_segment π x y = set.Ioo x y
theorem
open_segment_eq_Ioo'
{π : Type u_1}
[linear_ordered_field π]
{x y : π}
(hxy : x β y) :
open_segment π x y = set.Ioo (min x y) (max x y)
theorem
convex.mem_Ioc
{π : Type u_1}
[linear_ordered_field π]
{x y : π}
(h : x < y)
{z : π} :
A point is in an Ioc iff it can be expressed as a semistrict convex combination of the
endpoints.
theorem
convex.mem_Ico
{π : Type u_1}
[linear_ordered_field π]
{x y : π}
(h : x < y)
{z : π} :
A point is in an Ico iff it can be expressed as a semistrict convex combination of the
endpoints.
Convexity of sets #
def
convex
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
(s : set E) :
Prop
Convexity of sets.
theorem
convex_iff_segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{s : set E} :
theorem
convex.segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π 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_scalar π E]
{s : set E}
(h : convex π s)
{x y : E}
(hx : x β s)
(hy : y β s) :
open_segment π x y β s
theorem
convex_iff_pointwise_add_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{s : set E} :
Alternative definition of set convexity, in terms of pointwise set operations.
theorem
convex.set_combo_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{s : set E} :
Alias of convex_iff_pointwise_add_subset.
theorem
convex_empty
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E] :
theorem
convex_univ
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E] :
theorem
convex.inter
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{s t : set E}
(hs : convex π s)
(ht : convex π t) :
theorem
convex_sInter
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{S : set (set E)}
(h : β (s : set E), s β S β convex π s) :
theorem
convex_Inter
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{ΞΉ : Sort u_3}
{s : ΞΉ β set E}
(h : β (i : ΞΉ), convex π (s i)) :
convex π (β (i : ΞΉ), 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_scalar π E]
[has_scalar π F]
{s : set E}
{t : set F}
(hs : convex π s)
(ht : convex π t) :
theorem
convex_pi
{π : Type u_1}
[ordered_semiring π]
{ΞΉ : Type u_2}
{E : ΞΉ β Type u_3}
[Ξ (i : ΞΉ), add_comm_monoid (E i)]
[Ξ (i : ΞΉ), has_scalar π (E i)]
{s : set ΞΉ}
{t : Ξ (i : ΞΉ), set (E i)}
(ht : β (i : ΞΉ), convex π (t i)) :
theorem
directed.convex_Union
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π E]
{ΞΉ : Sort u_3}
{s : ΞΉ β set E}
(hdir : directed has_subset.subset s)
(hc : β β¦i : ΞΉβ¦, convex π (s i)) :
convex π (β (i : ΞΉ), s i)
theorem
directed_on.convex_sUnion
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_scalar π 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} :
@[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.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) :
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_interval
{π : 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.combo_eq_vadd
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_group E]
[module π E]
{a b : π}
{x y : E}
(h : a + b = 1) :
theorem
convex.sub
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_group E]
[module π E]
{s : set (E Γ E)}
(hs : convex π s) :
theorem
convex_segment
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_group E]
[module π E]
(x y : E) :
theorem
convex_open_segment
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_group E]
[module π E]
(a b : E) :
convex π (open_segment π a b)
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.add_smul_mem
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(hs : convex π s)
{x y : E}
(hx : x β s)
(hy : x + y β s)
{t : π}
(ht : t β set.Icc 0 1) :
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
convex.add_smul_sub_mem
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(h : convex π s)
{x y : E}
(hx : x β s)
(hy : y β 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.combo_affine_apply
{π : 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]
{a b : π}
{x y : E}
{f : E βα΅[π] F}
(h : a + b = 1) :
Applying an affine map to an affine combination of two points yields an affine combination of the images.
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]
(f : E βα΅[π] F)
{s : set E}
(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.neg_preimage
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(hs : convex π s) :
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
convex.add_smul
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{s : set E}
(h_conv : convex π s)
{p q : π}
(hp : 0 β€ p)
(hq : 0 β€ q) :
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 : zorn.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 convex_iff_ord_connected.
Convexity of submodules/subspaces #
theorem
submodule.convex
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(K : submodule π E) :
theorem
subspace.convex
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
(K : subspace π E) :
Simplex #
def
std_simplex
(π : Type u_1)
(ΞΉ : Type u_5)
[ordered_semiring π]
[fintype ΞΉ] :
set (ΞΉ β π)
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) β§ β (x : ΞΉ), f x = 1}
theorem
std_simplex_eq_inter
(π : Type u_1)
(ΞΉ : Type u_5)
[ordered_semiring π]
[fintype ΞΉ] :
std_simplex π ΞΉ = (β (x : ΞΉ), {f : ΞΉ β π | 0 β€ f x}) β© {f : ΞΉ β π | β (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 π ΞΉ