Jensen's inequality for conditional expectations

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

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

theorem MeasureTheory.enorm_condExp_le {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] (f : Ω → E) : ∀ᵐ (ω : Ω) ∂μ, ‖μ[f|m] ω‖ₑ ≤ ENNReal.ofReal (μ[fun (ω : Ω) => ‖f ω‖|m] ω)

theorem MeasureTheory.norm_rpow_condExp_le {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → E} [IsFiniteMeasure μ] {p : ENNReal} (one_le_p : 1 ≤ p) (p_ne_top : p ≠ ⊤) (hf : MemLp f p μ) : ∀ᵐ (ω : Ω) ∂μ, ‖μ[f|m] ω‖ ^ p.toReal ≤ μ[fun (ω : Ω) => ‖f ω‖ ^ p.toReal|m] ω

theorem MeasureTheory.enorm_rpow_condExp_le {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → E} [IsFiniteMeasure μ] {p : ENNReal} (one_le_p : 1 ≤ p) (p_ne_top : p ≠ ⊤) (hf : MemLp f p μ) : ∀ᵐ (ω : Ω) ∂μ, ‖μ[f|m] ω‖ₑ ^ p.toReal ≤ ENNReal.ofReal (μ[fun (ω : Ω) => ‖f ω‖ ^ p.toReal|m] ω)

theorem MeasureTheory.ofReal_condExp_norm_ae_le_eLpNormEssSup {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → E} [IsFiniteMeasure μ] (hf : AEStronglyMeasurable f μ) : ∀ᵐ (ω : Ω) ∂μ, ENNReal.ofReal (μ[fun (x : Ω) => ‖f x‖|m] ω) ≤ eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_condExp_le_eLpNorm {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {p : ENNReal} (hp : 1 ≤ p) (f : Ω → E) : eLpNorm μ[f|m] p μ ≤ eLpNorm f p μ

theorem MeasureTheory.MemLp.condExp' {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → E} [IsFiniteMeasure μ] {p : ENNReal} (hp : 1 ≤ p) (hf : MemLp f p μ) : MemLp μ[f|m] p μ

theorem MeasureTheory.ae_bdd_condExp_of_ae_bdd' {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {R : ℝ} {f : Ω → E} (hbdd : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ R) : ∀ᵐ (x : Ω) ∂μ, ‖μ[f|m] x‖ ≤ R

If a function f is bounded almost everywhere by R, then so is its conditional expectation.

theorem MeasureTheory.Integrable.uniformIntegrable_condExp' {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {ι : Type u_3} {g : Ω → E} (hint : Integrable g μ) {ℱ : ι → MeasurableSpace Ω} (hℱ : ∀ (i : ι), ℱ i ≤ mΩ) : UniformIntegrable (fun (i : ι) => μ[g|ℱ i]) 1 μ

Given an integrable function g, the conditional expectations of g with respect to a sequence of sub-σ-algebras is uniformly integrable.