mathlib documentation

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 convex_on.map_center_mass_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : convex_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : concave_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : convex_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (hf : concave_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} {x : E} {s : finset E} (hf : convex_on 𝕜 ((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} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E β} {x : E} {s : finset E} (hf : concave_on 𝕜 ((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} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (h : convex_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} {t : finset ι} {w : ι 𝕜} {p : ι E} (h : concave_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} (hf : convex_on 𝕜 ((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} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E β} (hf : concave_on 𝕜 ((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.