mathlib documentation

analysis.convex.integral

Jensen's inequality for integrals #

In this file we prove four theorems:

Tags #

convex, integral, center mass, Jensen's inequality

theorem convex.smul_integral_mem {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] [measure_theory.finite_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s) (hμ : μ 0) {f : α → E} (hfs : ∀ᵐ (x : α) ∂μ, f x s) (hfi : measure_theory.integrable f μ) :
((μ set.univ).to_real)⁻¹ (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: (μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s. See also convex.center_mass_mem for a finite sum version of this lemma.

theorem convex.integral_mem {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] [measure_theory.probability_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s) {f : α → E} (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_on.map_smul_integral_le {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] [measure_theory.finite_measure μ] {s : set E} {g : E → } (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ 0) {f : α → E} (hfs : ∀ᵐ (x : α) ∂μ, f x s) (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable (g f) μ) :
g (((μ set.univ).to_real)⁻¹ (x : α), f x μ) ((μ set.univ).to_real)⁻¹ (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.map_center_mass_le for a finite sum version of this lemma.

theorem convex_on.map_integral_le {α : Type u_1} {E : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] [measure_theory.probability_measure μ] {s : set E} {g : E → } (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E} (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.map_sum_le for a finite sum version of this lemma.