Conditional expectation of real-valued functions

This file proves some results regarding the conditional expectation of real-valued functions.

Main results

• MeasureTheory.rnDeriv_ae_eq_condExp: the conditional expectation μ[f | m] is equal to the Radon-Nikodym derivative of fμ restricted on m with respect to μ restricted on m.
• MeasureTheory.Integrable.uniformIntegrable_condExp: the conditional expectation of a function form a uniformly integrable class.

theorem MeasureTheory.rnDeriv_ae_eq_condExp {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [hμm : SigmaFinite (μ.trim hm)] {f : α → ℝ} (hf : Integrable f μ) : SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] μ[f | m]

theorem MeasureTheory.condExp_le_nonneg_const {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [PartialOrder E] [ClosedIciTopology E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {f : α → E} {c : E} (hc : 0 ≤ c) (hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c) : ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c

theorem MeasureTheory.abs_condExp_ae_le_condExp_abs {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] (f : α → E) : |μ[f | m]| ≤ᵐ[μ] μ[|f| | m]

theorem MeasureTheory.integral_abs_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] (f : α → E) : ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

theorem MeasureTheory.integral_condExp_le_of_ae_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) : ∫ (x : α), μ[f | m] x ∂μ ≤ ∫ (x : α), f x ∂μ

Note that this is not trivial as we don't assume that f is integrable.

theorem MeasureTheory.setIntegral_abs_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {s : Set α} (hs : MeasurableSet s) (f : α → E) : ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

theorem MeasureTheory.setIntegral_condExp_le_of_ae_restrict_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {f : α → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f) : ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

Note that this is not trivial as we don't assume that f is integrable.

theorem MeasureTheory.setIntegral_condExp_le_of_ae_nonneg {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) : ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

theorem MeasureTheory.ae_bdd_abs_condExp_of_ae_bdd_abs {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {R : E} {f : α → E} (hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ R) : ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ R

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

@[deprecated MeasureTheory.ae_bdd_abs_condExp_of_ae_bdd_abs (since := "2026-05-05")]

theorem MeasureTheory.ae_bdd_condExp_of_ae_bdd {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {R : NNReal} {f : α → ℝ} (hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) : ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

If the real-valued function f is bounded almost everywhere by R, then so is its conditional expectation.

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

theorem MeasureTheory.integral_norm_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : α → E) : ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ

theorem MeasureTheory.setIntegral_norm_condExp_rpow_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {p : ℝ} (hp : 1 ≤ p) {f : α → E} {s : Set α} (hs : MeasurableSet s) (hf : Integrable (fun (x : α) => ‖f x‖ ^ p) μ) : ∫ (x : α) in s, ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ

theorem MeasureTheory.setIntegral_norm_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {s : Set α} (hs : MeasurableSet s) (f : α → E) : ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

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

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

theorem MeasureTheory.MemLp.ae_norm_condExp_le_essSup {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : MemLp f ⊤ μ) : ∀ᵐ (x : α) ∂μ, ‖μ[f | m] x‖ ≤ essSup (fun (x : α) => ‖f x‖) μ

theorem MeasureTheory.MemLp.essSup_norm_condExp_le_essSup_norm {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NeZero μ] {f : α → E} (hf : MemLp f ⊤ μ) : essSup (fun (x : α) => ‖μ[f | m] x‖) μ ≤ essSup (fun (x : α) => ‖f x‖) μ

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

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

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

@[deprecated MeasureTheory.eLpNorm_condExp_le_eLpNorm (since := "2026-07-01")]

theorem MeasureTheory.eLpNorm_one_condExp_le_eLpNorm {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : α → E) : eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

theorem MeasureTheory.Integrable.uniformIntegrable_condExp {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Type u_2} [IsFiniteMeasure μ] {g : α → ℝ} (hint : Integrable g μ) {ℱ : ι → MeasurableSpace α} (hℱ : ∀ (i : ι), ℱ i ≤ m0) : 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.