mathlib documentation

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 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) :

Convex Jensen's inequality, finset.center_mass version.

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) :

Concave Jensen's inequality, finset.center_mass version.

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.

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 #

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.

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.

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.

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.