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 < Finset.sum t fun (i : ι) => w i) (hmem : it, p i s) :

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 < Finset.sum t fun (i : ι) => w i) (hmem : it, p i s) :

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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) :
f (Finset.sum t fun (i : ι) => w i p i) Finset.sum t fun (i : ι) => 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) :
(Finset.sum t fun (i : ι) => w i f (p i)) f (Finset.sum t fun (i : ι) => 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 + Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) (hv : 0 v) (hq : q s) :
f (v q + Finset.sum t fun (i : ι) => w i p i) v f q + Finset.sum t fun (i : ι) => 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 + Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) (hv : 0 v) (hq : q s) :
(v f q + Finset.sum t fun (i : ι) => w i f (p i)) f (v q + Finset.sum t fun (i : ι) => 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j p k) :
f (Finset.sum t fun (i : ι) => w i p i) < Finset.sum t fun (i : ι) => 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j p k) :
(Finset.sum t fun (i : ι) => w i f (p i)) < f (Finset.sum t fun (i : ι) => 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) (h_eq : (Finset.sum t fun (i : ι) => w i f (p i)) f (Finset.sum t fun (i : ι) => 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 in t, w i • p i) = ∑ i in 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) (h_eq : f (Finset.sum t fun (i : ι) => w i p i) Finset.sum t fun (i : ι) => 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 in t, w i • p i) = ∑ i in 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) :
(f (Finset.sum t fun (i : ι) => w i p i) = Finset.sum t fun (i : ι) => w i f (p i)) jt, p j = Finset.sum t fun (i : ι) => 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 in t, w i • p i) = ∑ i in 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) :
(f (Finset.sum t fun (i : ι) => w i p i) = Finset.sum t fun (i : ι) => w i f (p i)) jt, p j = Finset.sum t fun (i : ι) => 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 in t, w i • p i) = ∑ i in 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) :
(f (Finset.sum t fun (i : ι) => w i p i) = Finset.sum t fun (i : ι) => w i f (p i)) jt, w j 0p j = Finset.sum t fun (i : ι) => 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 in t, w i • p i) = ∑ i in 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₁ : (Finset.sum t fun (i : ι) => w i) = 1) (hmem : it, p i s) :
(f (Finset.sum t fun (i : ι) => w i p i) = Finset.sum t fun (i : ι) => w i f (p i)) jt, w j 0p j = Finset.sum t fun (i : ι) => 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 in t, w i • p i) = ∑ i in 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 le_sup_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : Eβ} {x : E} {s : Finset E} (hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f) (hx : x (convexHull 𝕜) s) :
f x Finset.sup' s (_ : s.Nonempty) f
theorem inf_le_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : Eβ} {x : E} {s : Finset E} (hf : ConcaveOn 𝕜 ((convexHull 𝕜) s) f) (hx : x (convexHull 𝕜) s) :
Finset.inf' s (_ : s.Nonempty) f f x
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β} {t : Finset ι} {w : ι𝕜} {p : ιE} (h : ConvexOn 𝕜 s f) (hw₀ : it, 0 w i) (hw₁ : 0 < Finset.sum t fun (i : ι) => w i) (hp : it, p i s) :
∃ i ∈ t, f (Finset.centerMass t 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β} {t : Finset ι} {w : ι𝕜} {p : ιE} (h : ConcaveOn 𝕜 s f) (hw₀ : it, 0 w i) (hw₁ : 0 < Finset.sum t fun (i : ι) => w i) (hp : it, p i s) :
∃ i ∈ t, f (p i) f (Finset.centerMass t 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β} (hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f) {x : E} (hx : x (convexHull 𝕜) s) :
∃ y ∈ s, 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β} (hf : ConcaveOn 𝕜 ((convexHull 𝕜) s) f) {x : E} (hx : x (convexHull 𝕜) s) :
∃ y ∈ s, 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 𝕜 β] {f : Eβ} {x : E} {y : E} {z : E} (hf : ConvexOn 𝕜 (segment 𝕜 x y) f) (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 𝕜 β] {f : Eβ} {x : E} {y : E} {z : E} (hf : ConcaveOn 𝕜 (segment 𝕜 x y) f) (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 𝕜 β] {f : 𝕜β} {x : 𝕜} {y : 𝕜} {z : 𝕜} (hf : ConvexOn 𝕜 (Set.Icc x y) f) (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 𝕜 β] {f : 𝕜β} {x : 𝕜} {y : 𝕜} {z : 𝕜} (hf : ConcaveOn 𝕜 (Set.Icc x y) f) (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.