Convex sets and functions on real vector spaces
In a real vector space, we define the following objects and properties.
segment x yis the closed segment joiningxandy.- A set
sisconvexif for any two pointsx y ∈ sit includessegment x y; - A function
f : E → βisconvex_ona setsifsis itself a convex set, and for any two pointsx y ∈ sthe segment joining(x, f x)to(y, f y)is (non-strictly) above the graph off; equivalently,convex_on f smeans that the epigraph{p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}is a convex set; - Center mass of a finite set of points with prescribed weights.
- Convex hull of a set
sis the minimal convex set that includess. - Standard simplex
std_simplex ι [fintype ι]is the intersection of the positive quadrant with the hyperplanes.sum = 1in the spaceι → ℝ.
We also provide various equivalent versions of the definitions above, prove that some specific sets are convex, and prove Jensen's inequality.
Note: To define convexity for functions f : E → β, we need β to be an ordered vector space,
defined using the instance ordered_semimodule ℝ β.
Notations
We use the following local notations:
I = Icc (0:ℝ) 1;[x, y] = segment x y.
They are defined using local notation, so they are not available outside of this file.
Segment
Convexity of sets
Examples of convex sets
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.
The translation of a convex set is also convex
The translation of a convex set is also convex
Convex functions
Convexity of functions
Concavity of functions
A function f is concave iff -f is convex
A function f is concave iff -f is convex
For a function on a convex set in a linear ordered space, in order to prove that it is convex
it suffices to verify the inequality f (a • x + b • y) ≤ a • f x + b • f y only for x < y
and positive a, b. The main use case is E = ℝ however one can apply it, e.g., to ℝ^n with
lexicographic order.
For a function on a convex set in a linear ordered space, in order to prove that it is concave
it suffices to verify the inequality a • f x + b • f y ≤ f (a • x + b • y) only for x < y
and positive a, b. The main use case is E = ℝ however one can apply it, e.g., to ℝ^n with
lexicographic order.
For a function f defined on a convex subset D of ℝ, if for any three points x<y<z
the slope of the secant line of f on [x, y] is less than or equal to the slope
of the secant line of f on [x, z], then f is convex on D. This way of proving convexity
of a function is used in the proof of convexity of a function with a monotone derivative.
For a function f defined on a convex subset D of ℝ, if for any three points x<y<z
the slope of the secant line of f on [x, y] is greater than or equal to the slope
of the secant line of f on [x, z], then f is concave on D.
A convex function on a segment is upper-bounded by the max of its endpoints.
A concave function on a segment is lower-bounded by the min of its endpoints.
A convex function on a segment is upper-bounded by the max of its endpoints.
A concave function on a segment is lower-bounded by the min of its endpoints.
If a function is convex on s, it remains convex when precomposed by an affine map
If a function is concave on s, it remains concave when precomposed by an affine map
If g is convex on s, so is (g ∘ f) on f ⁻¹' s for a linear f.
If g is concave on s, so is (g ∘ f) on f ⁻¹' s for a linear f.
If a function is convex on s, it remains convex after a translation.
If a function is concave on s, it remains concave after a translation.
If a function is convex on s, it remains convex after a translation.
If a function is concave on s, it remains concave after a translation.
Center mass of a finite collection of points with prescribed weights.
Note that we require neither 0 ≤ w i nor ∑ w = 1.
A convex combination of two centers of mass is a center of mass as well. This version deals with two different index types.
A convex combination of two centers of mass is a center of mass as well. This version works if two centers of mass share the set of original points.
Center mass of a finite subset of a convex set belongs to the set provided that all weights are non-negative, and the total weight is positive.
Jensen's inequality, finset.center_mass version.
Jensen's inequality, finset.sum version.
If a function f is convex on s takes value y at the center mass of some points
z i ∈ s, then for some i we have y ≤ f (z i).
Convex hull of a set s is the minimal convex set that includes s
Equations
- convex_hull s = ⋂ (t : set E) (hst : s ⊆ t) (ht : convex t), t
Convex hull of s is equal to the set of all centers of masses of finsets t, z '' t ⊆ s.
This version allows finsets in any type in any universe.
Maximum principle for convex functions. If a function f is convex on the convex hull of s,
then f can't have a maximum on convex_hull s outside of s.
Simplex
Standard simplex in the space of functions ι → ℝ is the set
of vectors with non-negative coordinates with total sum 1.
Equations
- std_simplex ι = {f : ι → ℝ | (∀ (x : ι), 0 ≤ f x) ∧ finset.univ.sum (λ (x : ι), f x) = 1}
std_simplex ι is the convex hull of the canonical basis in ι → ℝ.
Convex hull of a finite set is the image of the standard simplex in s → ℝ
under the linear map sending each function w to ∑ x in s, w x • x.
Since we have no sums over finite sets, we use sum over @finset.univ _ hs.fintype.
The map is defined in terms of operations on (s → ℝ) →ₗ[ℝ] ℝ so that later we will not need
to prove that this map is linear.
All values of a function f ∈ std_simplex ι belong to [0, 1].