Jensen's inequality for integrals

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

• for convex sets: Convex.average_mem, Convex.set_average_mem, Convex.integral_mem;

• for convex functions: ConvexOn.average_mem_epigraph, ConvexOn.map_average_le, ConvexOn.set_average_mem_epigraph, ConvexOn.map_set_average_le, ConvexOn.map_integral_le;

• for strictly convex sets: StrictConvex.ae_eq_const_or_average_mem_interior;

• for a closed ball in a strictly convex normed space: ae_eq_const_or_norm_integral_lt_of_norm_le_const;

• for strictly convex functions: StrictConvexOn.ae_eq_const_or_map_average_lt.

TODO

• Use a typeclass for strict convexity of a closed ball.

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 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsProbabilityMeasure μ] (hs : Convex ℝ s) (hsc : IsClosed s) (hf : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.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 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hs : Convex ℝ s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.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.centerMass_mem for a finite sum version of this lemma.

theorem Convex.set_average_mem {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} (hs : Convex ℝ s) (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ⊤) (hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) (hfi : MeasureTheory.IntegrableOn 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.centerMass_mem for a finite sum version of this lemma.

theorem Convex.set_average_mem_closure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} (hs : Convex ℝ s) (h0 : μ t ≠ 0) (ht : μ t ≠ ⊤) (hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) (hfi : MeasureTheory.IntegrableOn 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.centerMass_mem for a finite sum version of this lemma.

theorem ConvexOn.average_mem_epigraph {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.Integrable (g ∘ f) μ) : (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2}

theorem ConcaveOn.average_mem_hypograph {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.Integrable (g ∘ f) μ) : (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1}

theorem ConvexOn.map_average_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.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 ConvexOn.map_centerMass_le for a finite sum version of this lemma.

theorem ConcaveOn.le_map_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.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 ConcaveOn.le_map_centerMass for a finite sum version of this lemma.

theorem ConvexOn.set_average_mem_epigraph {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ⊤) (hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) (hfi : MeasureTheory.IntegrableOn f t μ) (hgi : MeasureTheory.IntegrableOn (g ∘ f) t μ) : (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2}

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 ConcaveOn.set_average_mem_hypograph {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ⊤) (hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) (hfi : MeasureTheory.IntegrableOn f t μ) (hgi : MeasureTheory.IntegrableOn (g ∘ f) t μ) : (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1}

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 ConvexOn.map_set_average_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ⊤) (hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) (hfi : MeasureTheory.IntegrableOn f t μ) (hgi : MeasureTheory.IntegrableOn (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 ConcaveOn.le_map_set_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ⊤) (hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) (hfi : MeasureTheory.IntegrableOn f t μ) (hgi : MeasureTheory.IntegrableOn (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 ConvexOn.map_integral_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.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 ConvexOn.map_centerMass_le for a finite sum version of this lemma.

theorem ConcaveOn.le_map_integral {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.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 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} [MeasureTheory.IsFiniteMeasure μ] (hfi : MeasureTheory.Integrable f μ) : f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ∃ (t : Set α), MeasurableSet 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 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} [MeasureTheory.IsFiniteMeasure μ] (hs : Convex ℝ s) (h0 : μ t ≠ 0) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.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 StrictConvex.ae_eq_const_or_average_mem_interior {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsFiniteMeasure μ] (hs : StrictConvex ℝ s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.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 StrictConvexOn.ae_eq_const_or_map_average_lt {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hg : StrictConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.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 StrictConcaveOn.ae_eq_const_or_lt_map_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hg : StrictConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s) (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.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 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {C : ℝ} [StrictConvexSpace ℝ 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 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {C : ℝ} [StrictConvexSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real Set.univ * 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 μ.real univ * C.

theorem ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {t : Set α} {f : α → E} {C : ℝ} [StrictConvexSpace ℝ 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 ∂μ‖ < μ.real t * 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 μ.real t * C.