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 offμrestricted onmwith respect toμrestricted onm.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)
:
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)
:
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)
:
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)
:
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)
:
Note that this is not trivial as we don't assume that f is integrable.
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)
:
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)
:
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) μ)
:
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)
:
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) μ)
:
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)
:
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)
:
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 ⊤ μ)
:
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 ⊤ μ)
:
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 μ)
:
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 μ)
:
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)
:
@[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)
:
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.