# mathlibdocumentation

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:

• 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 t0 w i) (h₁ : 0 < t.sum (λ (i : ι), w i)) (hmem : ∀ (i : ι), i tp 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 t0 w i) (h₁ : 0 < t.sum (λ (i : ι), w i)) (hmem : ∀ (i : ι), i tp 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 t0 w i) (h₁ : t.sum (λ (i : ι), w i) = 1) (hmem : ∀ (i : ι), i tp 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 t0 w i) (h₁ : t.sum (λ (i : ι), w i) = 1) (hmem : ∀ (i : ι), i tp 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 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 t0 w i) (hw₁ : 0 < t.sum (λ (i : ι), w i)) (hp : ∀ (i : ι), i tp 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 t0 w i) (hw₁ : 0 < t.sum (λ (i : ι), w i)) (hp : ∀ (i : ι), i tp 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.