Conditional Jensen's Inequality

This file contains the conditional Jensen's inequality. We follow the proof in [Hytonen_VanNeerven_Veraar_Wies_2016].

Main Statement

• Convex.condExp_mem : in a Banach space E with a finite measure μ, if f lies in a closed convex set s a.e., then μ[f | m] lies in s a.e.
• ConvexOn.map_condExp_le_univ: in a Banach space E with a sigma finite measure μ, if φ : E → ℝ is a convex lower-semicontinuous function, then for any f : α → E such that f and φ ∘ f are integrable, we have φ (𝔼[f | m]) ≤ 𝔼[φ ∘ f | m] a.e.

theorem Convex.condExp_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hf_int : MeasureTheory.Integrable f μ) (hs : IsClosed s) (hc : Convex ℝ s) (hf : ∀ᵐ (a : α) ∂μ, f a ∈ s) : ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

If f lies in a closed convex set s a.e., then μ[f | m] lies in s a.e.

theorem ConvexOn.map_condExp_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConvexOn ℝ s φ) (hφ_cont : LowerSemicontinuousOn φ s) (hf : ∀ᵐ (a : α) ∂μ, f a ∈ s) (hs : IsClosed s) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Conditional Jensen's inequality: in a Banach space E with a measure μ that is σ-finite on a sub-σ-algebra m, if φ : E → ℝ is convex and lower-semicontinuous on a closed set s, then for any f : α → E such that f and φ ∘ f are integrable, and f lies in s a.e., we have φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m].

theorem ConvexOn.map_condExp_le_trim {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} {mE : MeasurableSpace E} [BorelSpace E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConvexOn ℝ s φ) (hφ_cont : LowerSemicontinuousOn φ s) (hφ_meas : MeasureTheory.StronglyMeasurable φ) (hf : ∀ᵐ (a : α) ∂μ, f a ∈ s) (hs : IsClosed s) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m]

theorem ConcaveOn.condExp_map_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ s φ) (hφ_cont : UpperSemicontinuousOn φ s) (hf : ∀ᵐ (a : α) ∂μ, f a ∈ s) (hs : IsClosed s) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]

theorem ConcaveOn.condExp_map_le_trim {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} {mE : MeasurableSpace E} [BorelSpace E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ s φ) (hφ_cont : UpperSemicontinuousOn φ s) (hφ_meas : MeasureTheory.StronglyMeasurable φ) (hf : ∀ᵐ (a : α) ∂μ, f a ∈ s) (hs : IsClosed s) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m]

theorem ConvexOn.map_condExp_le_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConvexOn ℝ Set.univ φ) (hφ_cont : LowerSemicontinuous φ) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Conditional Jensen's inequality: in a Banach space E with a measure μ that is σ-finite on a sub-σ-algebra m, if φ : E → ℝ is convex and lower-semicontinuous, then for any f : α → E such that f and φ ∘ f are integrable, we have φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m].

theorem ConvexOn.map_condExp_le_trim_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mE : MeasurableSpace E} [BorelSpace E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConvexOn ℝ Set.univ φ) (hφ_cont : LowerSemicontinuous φ) (hφ_meas : MeasureTheory.StronglyMeasurable φ) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m]

theorem ConcaveOn.condExp_map_le_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ Set.univ φ) (hφ_cont : UpperSemicontinuous φ) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]

theorem ConcaveOn.condExp_map_le_trim_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {mE : MeasurableSpace E} [BorelSpace E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ Set.univ φ) (hφ_cont : UpperSemicontinuous φ) (hφ_meas : MeasureTheory.StronglyMeasurable φ) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m]

theorem norm_condExp_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → E) : (fun (x : α) => ‖μ[f | m] x‖) ≤ᵐ[μ] μ[fun (x : α) => ‖f x‖ | m]

In a Banach space E with a measure μ, then for any f : α → E, we have ‖𝔼[f | m]‖ ≤ᵐ[μ] 𝔼[‖f‖ | m].

theorem Integrable.norm_condExp_rpow_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ℝ} (hp : 1 ≤ p) (hfint : MeasureTheory.Integrable (fun (x : α) => ‖f x‖ ^ p) μ) : (fun (x : α) => ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun (x : α) => ‖f x‖ ^ p | m]

theorem ConvexOn.map_condExp_le_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConvexOn ℝ Set.univ φ) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Conditional Jensen's inequality: in a finite dimensional Banach space E with a measure μ that is σ-finite on a sub-σ-algebra m, if φ : E → ℝ is convex, then for any f : α → E such that f and φ ∘ f are integrable, we have φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m].

theorem ConcaveOn.condExp_map_le_of_finiteDimensional {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E} {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ E] (hm : m ≤ mα) [MeasureTheory.SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ Set.univ φ) (hf_int : MeasureTheory.Integrable f μ) (hφ_int : MeasureTheory.Integrable (φ ∘ f) μ) : μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]