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}
[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)
:
f (Finset.centerMass t w p) ≤ 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}
[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)
:
Finset.centerMass t w (f ∘ p) ≤ f (Finset.centerMass t w p)
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)
:
f x ≤ Finset.sup' s (_ : Finset.Nonempty s) f
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)
:
Finset.inf' s (_ : Finset.Nonempty s) f ≤ f x
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)
:
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)
:
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.