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:

As corollaries, we get:

Jensen's inequality #

theorem ConvexOn.map_centerMass_le {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} (hf : ConvexOn 𝕜 s f) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (h₁ : 0 < Finset.sum t fun i => w i) (hmem : ∀ (i : ι), i ∈ t → p i ∈ s) :

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} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (h₁ : 0 < Finset.sum t fun i => w i) (hmem : ∀ (i : ι), i ∈ t → p i ∈ s) :

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} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} (hf : ConvexOn 𝕜 s f) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (h₁ : (Finset.sum t fun i => w i) = 1) (hmem : ∀ (i : ι), i ∈ t → p 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} [LinearOrderedField 𝕜] [AddCommGroup E] [OrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (h₁ : (Finset.sum t fun i => w i) = 1) (hmem : ∀ (i : ι), i ∈ t → p 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} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} {x : E} {s : Finset E} (hf : ConvexOn 𝕜 (↑(convexHull 𝕜) ↑s) f) (hx : x ∈ ↑(convexHull 𝕜) ↑s) :
theorem inf_le_of_mem_convexHull {𝕜 : Type u_3} {E : Type u_1} {β : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} {x : E} {s : Finset E} (hf : ConcaveOn 𝕜 (↑(convexHull 𝕜) ↑s) f) (hx : x ∈ ↑(convexHull 𝕜) ↑s) :
theorem ConvexOn.exists_ge_of_centerMass {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} (h : ConvexOn 𝕜 s f) (hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (hw₁ : 0 < Finset.sum t fun i => w i) (hp : ∀ (i : ι), i ∈ t → p i ∈ s) :
∃ i, i ∈ t ∧ f (Finset.centerMass t 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 ConcaveOn.exists_le_of_centerMass {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} {ι : Type u_4} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} (h : ConcaveOn 𝕜 s f) (hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i) (hw₁ : 0 < Finset.sum t fun i => w i) (hp : ∀ (i : ι), i ∈ t → p i ∈ s) :
∃ i, i ∈ t ∧ f (p i) ≤ f (Finset.centerMass t 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 ConvexOn.exists_ge_of_mem_convexHull {𝕜 : Type u_3} {E : Type u_2} {β : Type u_1} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 (↑(convexHull 𝕜) s) f) {x : E} (hx : x ∈ ↑(convexHull 𝕜) 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} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 (↑(convexHull 𝕜) s) f) {x : E} (hx : x ∈ ↑(convexHull 𝕜) 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.