Jensen's inequality for integrals

In this file we prove four theorems:

convex.smul_integral_mem: 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.
convex.integral_mem: 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.
convex_on.map_smul_integral_le: 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.
convex_on.map_integral_le: 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.

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.

source

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.

source

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.

source

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.