Documentation

Mathlib.Analysis.Convex.Jensen

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:

As corollaries, we get:

Jensen's inequality #

theorem ConvexOn.map_centerMass_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : ConvexOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : 0 < it, w i) (hmem : it, p i s) :
f (t.centerMass w p) t.centerMass w (f p)

Convex Jensen's inequality, Finset.centerMass version.

theorem ConcaveOn.le_map_centerMass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : ConcaveOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : 0 < it, w i) (hmem : it, p i s) :
t.centerMass w (f p) f (t.centerMass w p)

Concave Jensen's inequality, Finset.centerMass version.

theorem ConvexOn.map_sum_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : ConvexOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : it, w i = 1) (hmem : it, p i s) :
f (∑ it, w i p i) it, w i f (p i)

Convex Jensen's inequality, Finset.sum version.

theorem ConcaveOn.le_map_sum {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : ConcaveOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : it, w i = 1) (hmem : it, p i s) :
it, w i f (p i) f (∑ it, w i p i)

Concave Jensen's inequality, Finset.sum version.

theorem ConvexOn.map_add_sum_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} {v : 𝕜} {q : E} (hf : ConvexOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : v + it, w i = 1) (hmem : it, p i s) (hv : 0 v) (hq : q s) :
f (v q + it, w i p i) v f q + it, w i f (p i)

Convex Jensen's inequality where an element plays a distinguished role.

theorem ConcaveOn.map_add_sum_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} {v : 𝕜} {q : E} (hf : ConcaveOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : v + it, w i = 1) (hmem : it, p i s) (hv : 0 v) (hq : q s) :
v f q + it, w i f (p i) f (v q + it, w i p i)

Concave Jensen's inequality where an element plays a distinguished role.

Strict Jensen inequality #

theorem StrictConvexOn.map_sum_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConvexOn 𝕜 s f) (h₀ : it, 0 < w i) (h₁ : it, w i = 1) (hmem : it, p i s) (hp : jt, kt, p j p k) :
f (∑ it, w i p i) < it, w i f (p i)

Convex strict Jensen inequality.

If the function is strictly convex, the weights are strictly positive and the indexed family of points is non-constant, then Jensen's inequality is strict.

See also StrictConvexOn.map_sum_eq_iff.

theorem StrictConcaveOn.lt_map_sum {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConcaveOn 𝕜 s f) (h₀ : it, 0 < w i) (h₁ : it, w i = 1) (hmem : it, p i s) (hp : jt, kt, p j p k) :
it, w i f (p i) < f (∑ it, w i p i)

Concave strict Jensen inequality.

If the function is strictly concave, the weights are strictly positive and the indexed family of points is non-constant, then Jensen's inequality is strict.

See also StrictConcaveOn.map_sum_eq_iff.

Equality case of Jensen's inequality #

theorem StrictConvexOn.eq_of_le_map_sum {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConvexOn 𝕜 s f) (h₀ : it, 0 < w i) (h₁ : it, w i = 1) (hmem : it, p i s) (h_eq : it, w i f (p i) f (∑ it, w i p i)) ⦃j : ι :
j t∀ ⦃k : ι⦄, k tp j = p k

A form of the equality case of Jensen's equality.

For a strictly convex function f and positive weights w, if f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i), then the points p are all equal.

See also StrictConvexOn.map_sum_eq_iff.

theorem StrictConcaveOn.eq_of_map_sum_eq {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConcaveOn 𝕜 s f) (h₀ : it, 0 < w i) (h₁ : it, w i = 1) (hmem : it, p i s) (h_eq : f (∑ it, w i p i) it, w i f (p i)) ⦃j : ι :
j t∀ ⦃k : ι⦄, k tp j = p k

A form of the equality case of Jensen's equality.

For a strictly concave function f and positive weights w, if f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i), then the points p are all equal.

See also StrictConcaveOn.map_sum_eq_iff.

theorem StrictConvexOn.map_sum_eq_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConvexOn 𝕜 s f) (h₀ : it, 0 < w i) (h₁ : it, w i = 1) (hmem : it, p i s) :
f (∑ it, w i p i) = it, w i f (p i) jt, p j = it, w i p i

Canonical form of the equality case of Jensen's equality.

For a strictly convex function f and positive weights w, we have f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) if and only if the points p are all equal (and in fact all equal to their center of mass wrt w).

theorem StrictConcaveOn.map_sum_eq_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConcaveOn 𝕜 s f) (h₀ : it, 0 < w i) (h₁ : it, w i = 1) (hmem : it, p i s) :
f (∑ it, w i p i) = it, w i f (p i) jt, p j = it, w i p i

Canonical form of the equality case of Jensen's equality.

For a strictly concave function f and positive weights w, we have f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) if and only if the points p are all equal (and in fact all equal to their center of mass wrt w).

theorem StrictConvexOn.map_sum_eq_iff' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConvexOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : it, w i = 1) (hmem : it, p i s) :
f (∑ it, w i p i) = it, w i f (p i) jt, w j 0p j = it, w i p i

Canonical form of the equality case of Jensen's equality.

For a strictly convex function f and nonnegative weights w, we have f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) if and only if the points p with nonzero weight are all equal (and in fact all equal to their center of mass wrt w).

theorem StrictConcaveOn.map_sum_eq_iff' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {t : Finset ι} {w : ι𝕜} {p : ιE} (hf : StrictConcaveOn 𝕜 s f) (h₀ : it, 0 w i) (h₁ : it, w i = 1) (hmem : it, p i s) :
f (∑ it, w i p i) = it, w i f (p i) jt, w j 0p j = it, w i p i

Canonical form of the equality case of Jensen's equality.

For a strictly concave function f and nonnegative weights w, we have f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) if and only if the points p with nonzero weight are all equal (and in fact all equal to their center of mass wrt w).

Maximum principle #

theorem ConvexOn.le_sup_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {t : Finset E} (hf : ConvexOn 𝕜 s f) (hts : t s) (hx : x (convexHull 𝕜) t) :
f x t.sup' f
theorem ConvexOn.inf_le_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {t : Finset E} (hf : ConcaveOn 𝕜 s f) (hts : t s) (hx : x (convexHull 𝕜) t) :
t.inf' f f x
@[deprecated ConvexOn.le_sup_of_mem_convexHull]
theorem le_sup_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {t : Finset E} (hf : ConvexOn 𝕜 s f) (hts : t s) (hx : x (convexHull 𝕜) t) :
f x t.sup' f

Alias of ConvexOn.le_sup_of_mem_convexHull.

@[deprecated ConvexOn.inf_le_of_mem_convexHull]
theorem inf_le_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {t : Finset E} (hf : ConcaveOn 𝕜 s f) (hts : t s) (hx : x (convexHull 𝕜) t) :
t.inf' f f x

Alias of ConvexOn.inf_le_of_mem_convexHull.

theorem ConvexOn.exists_ge_of_centerMass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {w : ι𝕜} {p : ιE} {t : Finset ι} (h : ConvexOn 𝕜 s f) (hw₀ : it, 0 w i) (hw₁ : 0 < it, w i) (hp : it, p i s) :
it, f (t.centerMass w p) f (p i)

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.

theorem ConcaveOn.exists_le_of_centerMass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {w : ι𝕜} {p : ιE} {t : Finset ι} (h : ConcaveOn 𝕜 s f) (hw₀ : it, 0 w i) (hw₁ : 0 < it, w i) (hp : it, p i s) :
it, f (p i) f (t.centerMass w p)

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.

theorem ConvexOn.exists_ge_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {t : Set E} (hf : ConvexOn 𝕜 s f) (hts : t s) (hx : x (convexHull 𝕜) t) :
yt, f x f y

Maximum principle for convex functions. If a function f is convex on the convex hull of s, then the eventual maximum of f on convexHull 𝕜 s lies in s.

theorem ConcaveOn.exists_le_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {t : Set E} (hf : ConcaveOn 𝕜 s f) (hts : t s) (hx : x (convexHull 𝕜) t) :
yt, f y f x

Minimum principle for concave functions. If a function f is concave on the convex hull of s, then the eventual minimum of f on convexHull 𝕜 s lies in s.

theorem ConvexOn.le_max_of_mem_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {y : E} {z : E} (hf : ConvexOn 𝕜 s f) (hx : x s) (hy : y s) (hz : z segment 𝕜 x y) :
f z max (f x) (f y)

Maximum principle for convex functions on a segment. If a function f is convex on the segment [x, y], then the eventual maximum of f on [x, y] is at x or y.

theorem ConcaveOn.min_le_of_mem_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : Eβ} {x : E} {y : E} {z : E} (hf : ConcaveOn 𝕜 s f) (hx : x s) (hy : y s) (hz : z segment 𝕜 x y) :
min (f x) (f y) f z

Minimum principle for concave functions on a segment. If a function f is concave on the segment [x, y], then the eventual minimum of f on [x, y] is at x or y.

theorem ConvexOn.le_max_of_mem_Icc {𝕜 : Type u_1} {β : Type u_4} [LinearOrderedField 𝕜] [LinearOrderedAddCommGroup β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set 𝕜} {f : 𝕜β} {x : 𝕜} {y : 𝕜} {z : 𝕜} (hf : ConvexOn 𝕜 s f) (hx : x s) (hy : y s) (hz : z Set.Icc x y) :
f z max (f x) (f y)

Maximum principle for convex functions on an interval. If a function f is convex on the interval [x, y], then the eventual maximum of f on [x, y] is at x or y.

theorem ConcaveOn.min_le_of_mem_Icc {𝕜 : Type u_1} {β : Type u_4} [LinearOrderedField 𝕜] [LinearOrderedAddCommGroup β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set 𝕜} {f : 𝕜β} {x : 𝕜} {y : 𝕜} {z : 𝕜} (hf : ConcaveOn 𝕜 s f) (hx : x s) (hy : y s) (hz : z Set.Icc x y) :
min (f x) (f y) f z

Minimum principle for concave functions on an interval. If a function f is concave on the interval [x, y], then the eventual minimum of f on [x, y] is at x or y.

theorem ConvexOn.bddAbove_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : Eβ} {s : Set E} {t : Set E} (hst : s t) (hf : ConvexOn 𝕜 t f) :
BddAbove (f '' s)BddAbove (f '' (convexHull 𝕜) s)
theorem ConcaveOn.bddBelow_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : Eβ} {s : Set E} {t : Set E} (hst : s t) (hf : ConcaveOn 𝕜 t f) :
BddBelow (f '' s)BddBelow (f '' (convexHull 𝕜) s)