Jensen's inequality for integrals #
In this file we prove several forms of Jensen's inequality for integrals.
-
for convex sets:
Convex.average_mem,Convex.set_average_mem,Convex.integral_mem; -
for convex functions:
ConvexOn.average_mem_epigraph,ConvexOn.map_average_le,ConvexOn.set_average_mem_epigraph,ConvexOn.map_set_average_le,ConvexOn.map_integral_le; -
for strictly convex sets:
StrictConvex.ae_eq_const_or_average_mem_interior; -
for a closed ball in a strictly convex normed space:
ae_eq_const_or_norm_integral_lt_of_norm_le_const; -
for strictly convex functions:
StrictConvexOn.ae_eq_const_or_map_average_lt.
TODO #
- Use a typeclass for strict convexity of a closed ball.
Tags #
convex, integral, center mass, average value, Jensen's inequality
Non-strict Jensen's inequality #
If μ is a probability measure on α, s is a convex closed set in E, and f is an
integrable function sending μ-a.e. points to s, then the expected value of f belongs to s:
∫ x, f x ∂μ ∈ s. See also Convex.sum_mem for a finite sum version of this lemma.
If μ is a non-zero finite measure on α, s is a convex closed set in E, and f is an
integrable function sending μ-a.e. points to s, then the average value of f belongs to s:
⨍ x, f x ∂μ ∈ s. See also Convex.centerMass_mem for a finite sum version of this lemma.
If μ is a non-zero finite measure on α, s is a convex closed set in E, and f is an
integrable function sending μ-a.e. points to s, then the average value of f belongs to s:
⨍ x, f x ∂μ ∈ s. See also Convex.centerMass_mem for a finite sum version of this lemma.
If μ is a non-zero finite measure on α, s is a convex set in E, and f is an integrable
function sending μ-a.e. points to s, then the average value of f belongs to closure s:
⨍ x, f x ∂μ ∈ s. See also Convex.centerMass_mem for a finite sum version of this lemma.
Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed
set s, μ is a finite non-zero measure on α, and f : α → E is a function sending
μ-a.e. points to s, then the value of g at the average value of f is less than or equal to
the average value of g ∘ f provided that both f and g ∘ f are integrable. See also
ConvexOn.map_centerMass_le for a finite sum version of this lemma.
Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed
set s, μ is a finite non-zero measure on α, and f : α → E is a function sending
μ-a.e. points to s, then the average value of g ∘ f is less than or equal to the value of g
at the average value of f provided that both f and g ∘ f are integrable. See also
ConcaveOn.le_map_centerMass for a finite sum version of this lemma.
Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed
set s, μ is a finite non-zero measure on α, and f : α → E is a function sending
μ-a.e. points of a set t to s, then the value of g at the average value of f over t is
less than or equal to the average value of g ∘ f over t provided that both f and g ∘ f are
integrable.
Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed
set s, μ is a finite non-zero measure on α, and f : α → E is a function sending
μ-a.e. points of a set t to s, then the average value of g ∘ f over t is less than or
equal to the value of g at the average value of f over t provided that both f and g ∘ f
are integrable.
Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed
set s, μ is a finite non-zero measure on α, and f : α → E is a function sending
μ-a.e. points of a set t to s, then the value of g at the average value of f over t is
less than or equal to the average value of g ∘ f over t provided that both f and g ∘ f are
integrable.
Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed
set s, μ is a finite non-zero measure on α, and f : α → E is a function sending
μ-a.e. points of a set t to s, then the average value of g ∘ f over t is less than or
equal to the value of g at the average value of f over t provided that both f and g ∘ f
are integrable.
Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed
set s, μ is a probability measure on α, and f : α → E is a function sending μ-a.e. points
to s, then the value of g at the expected value of f is less than or equal to the expected
value of g ∘ f provided that both f and g ∘ f are integrable. See also
ConvexOn.map_centerMass_le for a finite sum version of this lemma.
Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed
set s, μ is a probability measure on α, and f : α → E is a function sending μ-a.e. points
to s, then the expected value of g ∘ f is less than or equal to the value of g at the expected
value of f provided that both f and g ∘ f are integrable.
Strict Jensen's inequality #
If f : α → E is an integrable function, then either it is a.e. equal to the constant
⨍ x, f x ∂μ or there exists a measurable set such that μ t ≠ 0, μ tᶜ ≠ 0, and the average
values of f over t and tᶜ are different.
If an integrable function f : α → E takes values in a convex set s and for some set t of
positive measure, the average value of f over t belongs to the interior of s, then the average
of f over the whole space belongs to the interior of s.
If an integrable function f : α → E takes values in a strictly convex closed set s, then
either it is a.e. equal to its average value, or its average value belongs to the interior of
s.
Jensen's inequality, strict version: if an integrable function f : α → E takes values in a
convex closed set s, and g : E → ℝ is continuous and strictly convex on s, then
either f is a.e. equal to its average value, or g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ.
Jensen's inequality, strict version: if an integrable function f : α → E takes values in a
convex closed set s, and g : E → ℝ is continuous and strictly concave on s, then
either f is a.e. equal to its average value, or ⨍ x, g (f x) ∂μ < g (⨍ x, f x ∂μ).
If E is a strictly convex normed space and f : α → E is a function such that ‖f x‖ ≤ C
a.e., then either this function is a.e. equal to its average value, or the norm of its average value
is strictly less than C.
If E is a strictly convex normed space and f : α → E is a function such that ‖f x‖ ≤ C
a.e., then either this function is a.e. equal to its average value, or the norm of its integral is
strictly less than (μ univ).toReal * C.
If E is a strictly convex normed space and f : α → E is a function such that ‖f x‖ ≤ C
a.e. on a set t of finite measure, then either this function is a.e. equal to its average value on
t, or the norm of its integral over t is strictly less than (μ t).toReal * C.