Probabilistic properties of the conditional expectation #
This file contains some properties about the conditional expectation which does not belong in the main conditional expectation file.
Main result #
MeasureTheory.condExp_indep_eq: Ifm₁, m₂are independent σ-algebras andfis anm₁-measurable function, then𝔼[f | m₂] = 𝔼[f]almost everywhere.
theorem
MeasureTheory.condExp_indep_eq
{Ω : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace Real E]
[CompleteSpace E]
{m₁ m₂ m : MeasurableSpace Ω}
{μ : Measure Ω}
{f : Ω → E}
(hle₁ : LE.le m₁ m)
(hle₂ : LE.le m₂ m)
[SigmaFinite (μ.trim hle₂)]
(hf : StronglyMeasurable f)
(hindp : ProbabilityTheory.Indep m₁ m₂ μ)
:
(ae μ).EventuallyEq (condExp m₂ μ f) fun (x : Ω) => integral μ fun (x : Ω) => f x
If m₁, m₂ are independent σ-algebras and f is m₁-measurable, then 𝔼[f | m₂] = 𝔼[f]
almost everywhere.
@[deprecated MeasureTheory.condExp_indep_eq (since := "2025-01-21")]
theorem
MeasureTheory.condexp_indep_eq
{Ω : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace Real E]
[CompleteSpace E]
{m₁ m₂ m : MeasurableSpace Ω}
{μ : Measure Ω}
{f : Ω → E}
(hle₁ : LE.le m₁ m)
(hle₂ : LE.le m₂ m)
[SigmaFinite (μ.trim hle₂)]
(hf : StronglyMeasurable f)
(hindp : ProbabilityTheory.Indep m₁ m₂ μ)
:
(ae μ).EventuallyEq (condExp m₂ μ f) fun (x : Ω) => integral μ fun (x : Ω) => f x
Alias of MeasureTheory.condExp_indep_eq.
If m₁, m₂ are independent σ-algebras and f is m₁-measurable, then 𝔼[f | m₂] = 𝔼[f]
almost everywhere.