# Documentation

Mathlib.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:

• 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.

As corollaries, we get:

• 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_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} {t : } {w : ι𝕜} {p : ιE} (hf : ConvexOn 𝕜 s f) (h₀ : ∀ (i : ι), i t0 w i) (h₁ : 0 < Finset.sum t fun i => w i) (hmem : ∀ (i : ι), i tp i s) :
f () Finset.centerMass t w (f p)

Convex Jensen's inequality, Finset.centerMass version.

theorem ConcaveOn.le_map_centerMass {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} {t : } {w : ι𝕜} {p : ιE} (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ (i : ι), i t0 w i) (h₁ : 0 < Finset.sum t fun i => w i) (hmem : ∀ (i : ι), i tp i s) :
Finset.centerMass t w (f p) f ()

Concave Jensen's inequality, Finset.centerMass version.

theorem ConvexOn.map_sum_le {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} {t : } {w : ι𝕜} {p : ιE} (hf : ConvexOn 𝕜 s f) (h₀ : ∀ (i : ι), i t0 w i) (h₁ : (Finset.sum t fun i => w i) = 1) (hmem : ∀ (i : ι), i tp i s) :
f (Finset.sum t fun i => w i p i) Finset.sum t fun i => w i f (p i)

Convex Jensen's inequality, Finset.sum version.

theorem ConcaveOn.le_map_sum {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} {t : } {w : ι𝕜} {p : ιE} (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ (i : ι), i t0 w i) (h₁ : (Finset.sum t fun i => w i) = 1) (hmem : ∀ (i : ι), i tp i s) :
(Finset.sum t fun i => w i f (p i)) f (Finset.sum t fun i => w i p i)

Concave Jensen's inequality, Finset.sum version.

### Maximum principle #

theorem le_sup_of_mem_convexHull {𝕜 : Type u_3} {E : Type u_1} {β : Type u_2} [] [Module 𝕜 E] [Module 𝕜 β] [] {f : Eβ} {x : E} {s : } (hf : ConvexOn 𝕜 (↑() s) f) (hx : x ↑() s) :
f x Finset.sup' s (_ : ) f
theorem inf_le_of_mem_convexHull {𝕜 : Type u_3} {E : Type u_1} {β : Type u_2} [] [Module 𝕜 E] [Module 𝕜 β] [] {f : Eβ} {x : E} {s : } (hf : ConcaveOn 𝕜 (↑() s) f) (hx : x ↑() s) :
Finset.inf' s (_ : ) f f x
theorem ConvexOn.exists_ge_of_centerMass {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} {t : } {w : ι𝕜} {p : ιE} (h : ConvexOn 𝕜 s f) (hw₀ : ∀ (i : ι), i t0 w i) (hw₁ : 0 < Finset.sum t fun i => w i) (hp : ∀ (i : ι), i tp i s) :
i, i t f () 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_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} {t : } {w : ι𝕜} {p : ιE} (h : ConcaveOn 𝕜 s f) (hw₀ : ∀ (i : ι), i t0 w i) (hw₁ : 0 < Finset.sum t fun i => w i) (hp : ∀ (i : ι), i tp i s) :
i, i t f (p i) f ()

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_3} {E : Type u_2} {β : Type u_1} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} (hf : ConvexOn 𝕜 (↑() s) f) {x : E} (hx : x ↑() s) :
y, 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 convexHull 𝕜 s lies in s.

theorem ConcaveOn.exists_le_of_mem_convexHull {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} (hf : ConcaveOn 𝕜 (↑() s) f) {x : E} (hx : x ↑() s) :
y, 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 convexHull 𝕜 s lies in s.