# 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} [linear_ordered_field π] [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) :

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 π] [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) :

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 π] [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 π] [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 convex_on.exists_ge_of_center_mass {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} {ΞΉ : Type u_5} [linear_ordered_field π] [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 π] [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 π] [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 π] [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.