Jensen's inequality for conditional expectations

theorem MeasureTheory.enorm_condExp_le {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} (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.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.