English
If m1 ⊆ m2 ⊆ m0 and the trimmed μ-measure is sigma-finite, then conditioning first on m2 and then on m1 gives the same result as conditioning directly on m1, a.e.
Русский
Если m1 ⊆ m2 ⊆ m0 и после обрезки меры μ по hm2 получено сигма-конечное, то сначала условное ожидание по m2, затем по m1 эквивалентно условному по m1, почти наверняка.
LaTeX
$$$\mu[\mu[f|m_2]|m_1] =^{\mathrm{ae}}_{\mu} \mu[f|m_1]$$$
Lean4
/-- **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. -/
theorem condExp_condExp_of_le {m₁ m₂ m₀ : MeasurableSpace α} {μ : Measure α} (hm₁₂ : m₁ ≤ m₂) (hm₂ : m₂ ≤ m₀)
[SigmaFinite (μ.trim hm₂)] : μ[μ[f|m₂]|m₁] =ᵐ[μ] μ[f|m₁] :=
by
by_cases hμm₁ : SigmaFinite (μ.trim (hm₁₂.trans hm₂))
swap; · simp_rw [condExp_of_not_sigmaFinite (hm₁₂.trans hm₂) hμm₁]; rfl
by_cases hf : Integrable f μ
swap; · simp_rw [condExp_of_not_integrable hf, condExp_zero]; rfl
refine
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm₁₂.trans hm₂) (fun s _ _ => integrable_condExp.integrableOn)
(fun s _ _ => integrable_condExp.integrableOn) ?_ stronglyMeasurable_condExp.aestronglyMeasurable
stronglyMeasurable_condExp.aestronglyMeasurable
intro s hs _
rw [setIntegral_condExp (hm₁₂.trans hm₂) integrable_condExp hs]
rw [setIntegral_condExp (hm₁₂.trans hm₂) hf hs, setIntegral_condExp hm₂ hf (hm₁₂ s hs)]
