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 ℝ E]
[CompleteSpace E]
{m₁ : MeasurableSpace Ω}
{m₂ : MeasurableSpace Ω}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → E}
(hle₁ : m₁ ≤ m)
(hle₂ : m₂ ≤ m)
[MeasureTheory.SigmaFinite (μ.trim hle₂)]
(hf : MeasureTheory.StronglyMeasurable f)
(hindp : ProbabilityTheory.Indep m₁ m₂ μ)
:
MeasureTheory.condexp m₂ μ f =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), f x ∂μ
If m₁, m₂ are independent σ-algebras and f is m₁-measurable, then 𝔼[f | m₂] = 𝔼[f]
almost everywhere.