English
If the restriction of two σ-algebras m and m2 to a measurable set s agree in the sense described, then the conditional expectations of any integrable function f with respect to m and m2 are almost everywhere equal on s.
Русский
Если ограничения двух σ-алгебр m и m2 на множество s совпадают в описанном смысле, то CondExp по f относительно m и m2 совпадают почти повсеместно на s.
LaTeX
$$$$ \\mu[f|m] =_{a.e.,\\mu|s} \\mu[f|m_2] $$$$
Lean4
theorem condExp_ae_eq_restrict_zero (hs : MeasurableSet[m] s) (hf : f =ᵐ[μ.restrict s] 0) : μ[f|m] =ᵐ[μ.restrict s] 0 :=
by
by_cases hm : m ≤ m0
swap; · simp_rw [condExp_of_not_le hm]; rfl
by_cases hμm : SigmaFinite (μ.trim hm)
swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl
haveI : SigmaFinite (μ.trim hm) := hμm
have : SigmaFinite ((μ.restrict s).trim hm) :=
by
rw [← restrict_trim hm _ hs]
exact Restrict.sigmaFinite _ s
by_cases hf_int : Integrable f μ
swap; · rw [condExp_of_not_integrable hf_int]
refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_
· exact fun t _ _ => integrable_condExp.integrableOn.integrableOn
· exact fun t _ _ => (integrable_zero _ _ _).integrableOn
· intro t ht _
rw [Measure.restrict_restrict (hm _ ht), setIntegral_condExp hm hf_int (ht.inter hs), ←
Measure.restrict_restrict (hm _ ht)]
refine setIntegral_congr_ae (hm _ ht) ?_
filter_upwards [hf] with x hx _ using hx
· exact stronglyMeasurable_condExp.aestronglyMeasurable
· exact stronglyMeasurable_zero.aestronglyMeasurable
