Jensen's inequality and maximum principle for convex functions #
In this file, we prove the finite Jensen inequality and the finite maximum principle for convex
functions. The integral versions are to be found in analysis.convex.integral
.
Main declarations #
Jensen's inequalities:
convex_on.map_center_mass_le
,convex_on.map_sum_le
: Convex Jensen's inequality. The image of a convex combination of points under a convex function is less than the convex combination of the images.concave_on.le_map_center_mass
,concave_on.le_map_sum
: Concave Jensen's inequality.
As corollaries, we get:
convex_on.exists_ge_of_mem_convex_hull
: Maximum principle for convex functions.concave_on.exists_le_of_mem_convex_hull
: Minimum principle for concave functions.
Jensen's inequality #
Convex Jensen's inequality, finset.center_mass
version.
Concave Jensen's inequality, finset.center_mass
version.
Convex Jensen's inequality, finset.sum
version.
Concave Jensen's inequality, finset.sum
version.
Maximum principle #
If a function f
is convex on s
, then the value it takes at some center of mass of points of
s
is less than the value it takes on one of those points.
If a function f
is concave on s
, then the value it takes at some center of mass of points of
s
is greater than the value it takes on one of those points.
Maximum principle for convex functions. If a function f
is convex on the convex hull of s
,
then the eventual maximum of f
on convex_hull π s
lies in s
.
Minimum principle for concave functions. If a function f
is concave on the convex hull of s
,
then the eventual minimum of f
on convex_hull π s
lies in s
.