mathlib3 documentation

analysis.convex.integral

Jensen's inequality for integrals #

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

In this file we prove several forms of Jensen's inequality for integrals.

TODO #

Tags #

convex, integral, center mass, average value, Jensen's inequality

Non-strict Jensen's inequality #

theorem convex.integral_mem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} [measure_theory.is_probability_measure μ] (hs : convex s) (hsc : is_closed s) (hf : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) :
(x : α), f x μ s

If μ is a probability measure on α, s is a convex closed set in E, and f is an integrable function sending μ-a.e. points to s, then the expected value of f belongs to s: ∫ x, f x ∂μ ∈ s. See also convex.sum_mem for a finite sum version of this lemma.

theorem convex.average_mem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} [measure_theory.is_finite_measure μ] (hs : convex s) (hsc : is_closed s) (hμ : μ 0) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) :
(x : α), f x μ s

If μ is a non-zero finite measure on α, s is a convex closed set in E, and f is an integrable function sending μ-a.e. points to s, then the average value of f belongs to s: ⨍ x, f x ∂μ ∈ s. See also convex.center_mass_mem for a finite sum version of this lemma.

theorem convex.set_average_mem {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} (hs : convex s) (hsc : is_closed s) (h0 : μ t 0) (ht : μ t ) (hfs : ∀ᵐ (x : α) μ.restrict t, f x s) (hfi : measure_theory.integrable_on f t μ) :
(x : α) in t, f x μ s

If μ is a non-zero finite measure on α, s is a convex closed set in E, and f is an integrable function sending μ-a.e. points to s, then the average value of f belongs to s: ⨍ x, f x ∂μ ∈ s. See also convex.center_mass_mem for a finite sum version of this lemma.

theorem convex.set_average_mem_closure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} (hs : convex s) (h0 : μ t 0) (ht : μ t ) (hfs : ∀ᵐ (x : α) μ.restrict t, f x s) (hfi : measure_theory.integrable_on f t μ) :
(x : α) in t, f x μ closure s

If μ is a non-zero finite measure on α, s is a convex set in E, and f is an integrable function sending μ-a.e. points to s, then the average value of f belongs to closure s: ⨍ x, f x ∂μ ∈ s. See also convex.center_mass_mem for a finite sum version of this lemma.

theorem convex_on.average_mem_epigraph {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_finite_measure μ] (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ 0) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
( (x : α), f x μ, (x : α), g (f x) μ) {p : E × | p.fst s g p.fst p.snd}
theorem concave_on.average_mem_hypograph {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_finite_measure μ] (hg : concave_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ 0) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
( (x : α), f x μ, (x : α), g (f x) μ) {p : E × | p.fst s p.snd g p.fst}
theorem convex_on.map_average_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_finite_measure μ] (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ 0) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
g ( (x : α), f x μ) (x : α), g (f x) μ

Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed set s, μ is a finite non-zero measure on α, and f : α → E is a function sending μ-a.e. points to s, then the value of g at the average value of f is less than or equal to the average value of g ∘ f provided that both f and g ∘ f are integrable. See also convex_on.map_center_mass_le for a finite sum version of this lemma.

theorem concave_on.le_map_average {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_finite_measure μ] (hg : concave_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ 0) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
(x : α), g (f x) μ g ( (x : α), f x μ)

Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed set s, μ is a finite non-zero measure on α, and f : α → E is a function sending μ-a.e. points to s, then the average value of g ∘ f is less than or equal to the value of g at the average value of f provided that both f and g ∘ f are integrable. See also concave_on.le_map_center_mass for a finite sum version of this lemma.

theorem convex_on.set_average_mem_epigraph {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} {g : E } (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (h0 : μ t 0) (ht : μ t ) (hfs : ∀ᵐ (x : α) μ.restrict t, f x s) (hfi : measure_theory.integrable_on f t μ) (hgi : measure_theory.integrable_on (g f) t μ) :
( (x : α) in t, f x μ, (x : α) in t, g (f x) μ) {p : E × | p.fst s g p.fst p.snd}

Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed set s, μ is a finite non-zero measure on α, and f : α → E is a function sending μ-a.e. points of a set t to s, then the value of g at the average value of f over t is less than or equal to the average value of g ∘ f over t provided that both f and g ∘ f are integrable.

theorem concave_on.set_average_mem_hypograph {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} {g : E } (hg : concave_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (h0 : μ t 0) (ht : μ t ) (hfs : ∀ᵐ (x : α) μ.restrict t, f x s) (hfi : measure_theory.integrable_on f t μ) (hgi : measure_theory.integrable_on (g f) t μ) :
( (x : α) in t, f x μ, (x : α) in t, g (f x) μ) {p : E × | p.fst s p.snd g p.fst}

Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed set s, μ is a finite non-zero measure on α, and f : α → E is a function sending μ-a.e. points of a set t to s, then the average value of g ∘ f over t is less than or equal to the value of g at the average value of f over t provided that both f and g ∘ f are integrable.

theorem convex_on.map_set_average_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} {g : E } (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (h0 : μ t 0) (ht : μ t ) (hfs : ∀ᵐ (x : α) μ.restrict t, f x s) (hfi : measure_theory.integrable_on f t μ) (hgi : measure_theory.integrable_on (g f) t μ) :
g ( (x : α) in t, f x μ) (x : α) in t, g (f x) μ

Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed set s, μ is a finite non-zero measure on α, and f : α → E is a function sending μ-a.e. points of a set t to s, then the value of g at the average value of f over t is less than or equal to the average value of g ∘ f over t provided that both f and g ∘ f are integrable.

theorem concave_on.le_map_set_average {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} {g : E } (hg : concave_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (h0 : μ t 0) (ht : μ t ) (hfs : ∀ᵐ (x : α) μ.restrict t, f x s) (hfi : measure_theory.integrable_on f t μ) (hgi : measure_theory.integrable_on (g f) t μ) :
(x : α) in t, g (f x) μ g ( (x : α) in t, f x μ)

Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed set s, μ is a finite non-zero measure on α, and f : α → E is a function sending μ-a.e. points of a set t to s, then the average value of g ∘ f over t is less than or equal to the value of g at the average value of f over t provided that both f and g ∘ f are integrable.

theorem convex_on.map_integral_le {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_probability_measure μ] (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
g ( (x : α), f x μ) (x : α), g (f x) μ

Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed set s, μ is a probability measure on α, and f : α → E is a function sending μ-a.e. points to s, then the value of g at the expected value of f is less than or equal to the expected value of g ∘ f provided that both f and g ∘ f are integrable. See also convex_on.map_center_mass_le for a finite sum version of this lemma.

theorem concave_on.le_map_integral {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_probability_measure μ] (hg : concave_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
(x : α), g (f x) μ g ( (x : α), f x μ)

Jensen's inequality: if a function g : E → ℝ is concave and continuous on a convex closed set s, μ is a probability measure on α, and f : α → E is a function sending μ-a.e. points to s, then the expected value of g ∘ f is less than or equal to the value of g at the expected value of f provided that both f and g ∘ f are integrable.

Strict Jensen's inequality #

theorem ae_eq_const_or_exists_average_ne_compl {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {f : α E} [measure_theory.is_finite_measure μ] (hfi : measure_theory.integrable f μ) :
f =ᵐ[μ] function.const α ( (x : α), f x μ) (t : set α), measurable_set t μ t 0 μ t 0 (x : α) in t, f x μ (x : α) in t, f x μ

If f : α → E is an integrable function, then either it is a.e. equal to the constant ⨍ x, f x ∂μ or there exists a measurable set such that μ t ≠ 0, μ tᶜ ≠ 0, and the average values of f over t and tᶜ are different.

theorem convex.average_mem_interior_of_set {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {t : set α} {f : α E} [measure_theory.is_finite_measure μ] (hs : convex s) (h0 : μ t 0) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (ht : (x : α) in t, f x μ interior s) :
(x : α), f x μ interior s

If an integrable function f : α → E takes values in a convex set s and for some set t of positive measure, the average value of f over t belongs to the interior of s, then the average of f over the whole space belongs to the interior of s.

theorem strict_convex.ae_eq_const_or_average_mem_interior {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} [measure_theory.is_finite_measure μ] (hs : strict_convex s) (hsc : is_closed s) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) :
f =ᵐ[μ] function.const α ( (x : α), f x μ) (x : α), f x μ interior s

If an integrable function f : α → E takes values in a strictly convex closed set s, then either it is a.e. equal to its average value, or its average value belongs to the interior of s.

theorem strict_convex_on.ae_eq_const_or_map_average_lt {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_finite_measure μ] (hg : strict_convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
f =ᵐ[μ] function.const α ( (x : α), f x μ) g ( (x : α), f x μ) < (x : α), g (f x) μ

Jensen's inequality, strict version: if an integrable function f : α → E takes values in a convex closed set s, and g : E → ℝ is continuous and strictly convex on s, then either f is a.e. equal to its average value, or g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ.

theorem strict_concave_on.ae_eq_const_or_lt_map_average {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {s : set E} {f : α E} {g : E } [measure_theory.is_finite_measure μ] (hg : strict_concave_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hfs : ∀ᵐ (x : α) μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
f =ᵐ[μ] function.const α ( (x : α), f x μ) (x : α), g (f x) μ < g ( (x : α), f x μ)

Jensen's inequality, strict version: if an integrable function f : α → E takes values in a convex closed set s, and g : E → ℝ is continuous and strictly concave on s, then either f is a.e. equal to its average value, or ⨍ x, g (f x) ∂μ < g (⨍ x, f x ∂μ).

theorem ae_eq_const_or_norm_average_lt_of_norm_le_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {f : α E} {C : } [strict_convex_space E] (h_le : ∀ᵐ (x : α) μ, f x C) :
f =ᵐ[μ] function.const α ( (x : α), f x μ) (x : α), f x μ < C

If E is a strictly convex normed space and f : α → E is a function such that ‖f x‖ ≤ C a.e., then either this function is a.e. equal to its average value, or the norm of its average value is strictly less than C.

theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {f : α E} {C : } [strict_convex_space E] [measure_theory.is_finite_measure μ] (h_le : ∀ᵐ (x : α) μ, f x C) :
f =ᵐ[μ] function.const α ( (x : α), f x μ) (x : α), f x μ < (μ set.univ).to_real * C

If E is a strictly convex normed space and f : α → E is a function such that ‖f x‖ ≤ C a.e., then either this function is a.e. equal to its average value, or the norm of its integral is strictly less than (μ univ).to_real * C.

theorem ae_eq_const_or_norm_set_integral_lt_of_norm_le_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space E] [complete_space E] {μ : measure_theory.measure α} {t : set α} {f : α E} {C : } [strict_convex_space E] (ht : μ t ) (h_le : ∀ᵐ (x : α) μ.restrict t, f x C) :
f =ᵐ[μ.restrict t] function.const α ( (x : α) in t, f x μ) (x : α) in t, f x μ < (μ t).to_real * C

If E is a strictly convex normed space and f : α → E is a function such that ‖f x‖ ≤ C a.e. on a set t of finite measure, then either this function is a.e. equal to its average value on t, or the norm of its integral over t is strictly less than (μ t).to_real * C.