mathlib3documentation

analysis.convex.jensen

Jensen's inequality and maximum principle for convex functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

theorem convex_on.map_center_mass_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : s f) (h₀ : (i : ι), i t 0 w i) (h₁ : 0 < t.sum (λ (i : ι), w i)) (hmem : (i : ι), i t p i s) :
f (t.center_mass w p) t.center_mass w (f p)

Convex Jensen's inequality, finset.center_mass version.

theorem concave_on.le_map_center_mass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : s f) (h₀ : (i : ι), i t 0 w i) (h₁ : 0 < t.sum (λ (i : ι), w i)) (hmem : (i : ι), i t p i s) :
t.center_mass w (f p) f (t.center_mass w p)

Concave Jensen's inequality, finset.center_mass version.

theorem convex_on.map_sum_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : s f) (h₀ : (i : ι), i t 0 w i) (h₁ : t.sum (λ (i : ι), w i) = 1) (hmem : (i : ι), i t p i s) :
f (t.sum (λ (i : ι), w i p i)) t.sum (λ (i : ι), w i f (p i))

Convex Jensen's inequality, finset.sum version.

theorem concave_on.le_map_sum {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : s f) (h₀ : (i : ι), i t 0 w i) (h₁ : t.sum (λ (i : ι), w i) = 1) (hmem : (i : ι), i t p i s) :
t.sum (λ (i : ι), w i f (p i)) f (t.sum (λ (i : ι), w i p i))

Concave Jensen's inequality, finset.sum version.

Maximum principle #

theorem le_sup_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {f : E β} {x : E} {s : finset E} (hf : ((convex_hull 𝕜) s) f) (hx : x (convex_hull 𝕜) s) :
f x s.sup' _ f
theorem inf_le_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {f : E β} {x : E} {s : finset E} (hf : ((convex_hull 𝕜) s) f) (hx : x (convex_hull 𝕜) s) :
s.inf' _ f f x
theorem convex_on.exists_ge_of_center_mass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (h : s f) (hw₀ : (i : ι), i t 0 w i) (hw₁ : 0 < t.sum (λ (i : ι), w i)) (hp : (i : ι), i t p i s) :
(i : ι) (H : i t), f (t.center_mass 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 concave_on.exists_le_of_center_mass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (h : s f) (hw₀ : (i : ι), i t 0 w i) (hw₁ : 0 < t.sum (λ (i : ι), w i)) (hp : (i : ι), i t p i s) :
(i : ι) (H : i t), f (p i) f (t.center_mass 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 convex_on.exists_ge_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E β} (hf : ((convex_hull 𝕜) s) f) {x : E} (hx : x (convex_hull 𝕜) s) :
(y : E) (H : 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 convex_hull 𝕜 s lies in s.

theorem concave_on.exists_le_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E β} (hf : ((convex_hull 𝕜) s) f) {x : E} (hx : x (convex_hull 𝕜) s) :
(y : E) (H : 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 convex_hull 𝕜 s lies in s.