Theorems · Theorem · measure theory

MeasureTheory.condExp_condExp_of_le

∀ {α : Type u_1} {E : Type u_3} {f : α → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  {m₁ m₂ m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  m₁ ≤ m₂ → ∀ (hm₂ : m₂ ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm₂)], μ[μ[f | m₂] | m₁] =ᵐ[μ] μ[f | m₁]

Tower property of the conditional expectation. Taking the m₂-conditional expectation then the m₁-conditional expectation, where m₁ is a smaller σ-algebra, is the same as taking the m₁-conditional expectation directly.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Cited by

6 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasureTheory.SigmaFinite