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 #

source

theorem convex_on.map_center_mass_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [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) :

f (t.center_mass w p) ≤ t.center_mass w (f ∘ p)

Convex Jensen's inequality, finset.center_mass version.

source

theorem concave_on.le_map_center_mass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [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) :

t.center_mass w (f ∘ p) ≤ f (t.center_mass w p)

Concave Jensen's inequality, finset.center_mass version.

source

theorem convex_on.map_sum_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [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.

source

theorem concave_on.le_map_sum {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [ordered_add_comm_group β] [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 #

source

theorem convex_on.exists_ge_of_center_mass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [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.

source

theorem concave_on.exists_le_of_center_mass {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [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.

source

theorem convex_on.exists_ge_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [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.

source

theorem concave_on.exists_le_of_mem_convex_hull {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β] [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.