Convex sets and functions in vector spaces #
In a π-vector space, we define the following objects and properties.
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.
TODO #
Generalize all this file to affine spaces.
Convexity of sets #
Convexity of sets.
Equations
- convex π s = β β¦x : Eβ¦, x β s β star_convex π x s
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.
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}