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:

• ConvexOn.map_centerMass_le, ConvexOn.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.
• ConcaveOn.le_map_centerMass, ConcaveOn.le_map_sum: Concave Jensen's inequality.
• StrictConvexOn.map_sum_lt: Convex strict Jensen inequality.
• StrictConcaveOn.lt_map_sum: Concave strict Jensen inequality.

As corollaries, we get:

• StrictConvexOn.map_sum_eq_iff: Equality case of the convex Jensen inequality.
• StrictConcaveOn.map_sum_eq_iff: Equality case of the concave Jensen inequality.
• ConvexOn.exists_ge_of_mem_convexHull: Maximum principle for convex functions.
• ConcaveOn.exists_le_of_mem_convexHull: Minimum principle for concave functions.

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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : 0 < ∑ i ∈ t, w i) (hmem : ∀ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : 0 < ∑ i ∈ t, w i) (hmem : ∀ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : v + ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (hv : 0 ≤ v) (hq : q ∈ s) : f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : v + ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (hv : 0 ≤ v) (hq : q ∈ s) : v • f q + ∑ i ∈ t, w i • f (p i) ≤ f (v • q + ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) : f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) : ∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)) ⦃j : ι⦄ : j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p 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₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)) ⦃j : ι⦄ : j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p 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₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ t, w i) (hp : ∀ i ∈ t, p i ∈ s) : ∃ i ∈ t, 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₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ t, w i) (hp : ∀ i ∈ t, p i ∈ s) : ∃ i ∈ t, 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) : ∃ y ∈ t, 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) : ∃ y ∈ t, 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 y z : E} (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ segment 𝕜 x y) : f z ≤ 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 y z : E} (hf : ConcaveOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ segment 𝕜 x y) : 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 ≤ 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) : 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 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 t : Set E} (hst : s ⊆ t) (hf : ConcaveOn 𝕜 t f) : BddBelow (f '' s) → BddBelow (f '' (convexHull 𝕜) s)