Convex sets and functions in vector spaces #
In a π-vector space, we define the following objects and properties.
segment π x y
: Closed segment joiningx
andy
.open_segment π x y
: Open segment joiningx
andy
.convex π s
: A sets
is convex if for any two pointsx y β s
it 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 #
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
.
A point is in an Ioc
iff it can be expressed as a semistrict convex combination of the
endpoints.
A point is in an Ico
iff it can be expressed as a semistrict convex combination of the
endpoints.
Convexity of sets #
Convexity of sets.
Alternative definition of set convexity, in terms of pointwise set operations.
Alias of the forward direction of convex_iff_pointwise_add_subset`.
The translation of a convex set is also convex.
The translation of a convex set is also convex.
Affine subspaces are convex.
Applying an affine map to an affine combination of two points yields an affine combination of the images.
The preimage of a convex set under an affine map is convex.
The image of a convex set under an affine map is convex.
Alternative definition of set convexity, using division.
Alias of the forward direction of convex_iff_ord_connected`.
Convexity of submodules/subspaces #
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}