Jensen's inequality and maximum principle for convex functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 le_sup_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 𝕜 β] {f : E → β} {x : E} {s : finset E} (hf : convex_on 𝕜 (⇑(convex_hull 𝕜) ↑s) f) (hx : x ∈ ⇑(convex_hull 𝕜) ↑s) :

f x ≤ s.sup' _ f

source

theorem inf_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 𝕜 β] {f : E → β} {x : E} {s : finset E} (hf : concave_on 𝕜 (⇑(convex_hull 𝕜) ↑s) f) (hx : x ∈ ⇑(convex_hull 𝕜) ↑s) :

s.inf' _ f ≤ f x

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.