# mathlibdocumentation

analysis.convex.integral

# 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} {μ : measure_theory.measure α} [normed_group E] [ E] [borel_space E] {s : set E} (hs : convex s) (hsc : is_closed s) (hμ : μ 0) {f : α → E} (hfs : ∀ᵐ (x : α) ∂μ, f x s) (hfi : μ) :
((μ 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} {μ : measure_theory.measure α} [normed_group E] [ E] [borel_space E] {s : set E} (hs : convex s) (hsc : is_closed s) {f : α → E} (hf : ∀ᵐ (x : α) ∂μ, f x s) (hfi : μ) :
(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} {μ : measure_theory.measure α} [normed_group E] [ E] [borel_space E] {s : set E} {g : E → } (hg : g) (hgc : s) (hsc : is_closed s) (hμ : μ 0) {f : α → E} (hfs : ∀ᵐ (x : α) ∂μ, f x s) (hfi : μ) (hgi : μ) :
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} {μ : measure_theory.measure α} [normed_group E] [ E] [borel_space E] {s : set E} {g : E → } (hg : g) (hgc : s) (hsc : is_closed s) {f : α → E} (hfs : ∀ᵐ (x : α) ∂μ, f x s) (hfi : μ) (hgi : μ) :
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.