English
If m ≤ m0 and the σ-finiteness condition holds, the conditional expectation over μ restricted to s agrees almost surely with the restricted conditional expectation over μ on the same set, for integrable f.
Русский
При m ≤ m0 и условии сигма-финитности CondExp по μ на s совпадает почти повсюду с CondExp по ограниченной μ на той же множестве.
LaTeX
$$$$ (\\mu|_s)[f|m] =_{a.e.} (\\mu|_s)[f|m] $$$$
Lean4
/-- If the restriction to an `m`-measurable set `s` of a σ-algebra `m` is equal to the restriction
to `s` of another σ-algebra `m₂` (hypothesis `hs`), then `μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂]`. -/
theorem condExp_ae_eq_restrict_of_measurableSpace_eq_on {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0)
(hm₂ : m₂ ≤ m0) [SigmaFinite (μ.trim hm)] [SigmaFinite (μ.trim hm₂)] (hs_m : MeasurableSet[m] s)
(hs : ∀ t, MeasurableSet[m] (s ∩ t) ↔ MeasurableSet[m₂] (s ∩ t)) : μ[f|m] =ᵐ[μ.restrict s] μ[f|m₂] :=
by
rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]
have hs_m₂ : MeasurableSet[m₂] s := by rwa [← Set.inter_univ s, ← hs Set.univ, Set.inter_univ]
by_cases hf_int : Integrable f μ
swap; · simp_rw [condExp_of_not_integrable hf_int]; rfl
refine ((condExp_indicator hf_int hs_m).symm.trans ?_).trans (condExp_indicator hf_int hs_m₂)
refine
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm₂ (fun s _ _ => integrable_condExp.integrableOn)
(fun s _ _ => integrable_condExp.integrableOn) ?_ ?_ stronglyMeasurable_condExp.aestronglyMeasurable
swap
· have : StronglyMeasurable[m] (μ[s.indicator f|m]) := stronglyMeasurable_condExp
refine this.aestronglyMeasurable.of_measurableSpace_le_on hm hs_m (fun t => (hs t).mp) ?_
exact condExp_ae_eq_restrict_zero hs_m.compl (indicator_ae_eq_restrict_compl (hm _ hs_m))
intro t ht _
have : ∫ x in t, (μ[s.indicator f|m]) x ∂μ = ∫ x in s ∩ t, (μ[s.indicator f|m]) x ∂μ :=
by
rw [← integral_add_compl (hm _ hs_m) integrable_condExp.integrableOn]
suffices ∫ x in sᶜ, (μ[s.indicator f|m]) x ∂μ.restrict t = 0 by
rw [this, add_zero, Measure.restrict_restrict (hm _ hs_m)]
rw [Measure.restrict_restrict (MeasurableSet.compl (hm _ hs_m))]
suffices μ[s.indicator f|m] =ᵐ[μ.restrict sᶜ] 0
by
rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
calc
∫ x : α in t, (μ[s.indicator f|m]) x ∂μ.restrict sᶜ = ∫ x : α in t, 0 ∂μ.restrict sᶜ :=
by
refine setIntegral_congr_ae (hm₂ _ ht) ?_
filter_upwards [this] with x hx _ using hx
_ = 0 := integral_zero _ _
refine condExp_ae_eq_restrict_zero hs_m.compl ?_
exact indicator_ae_eq_restrict_compl (hm _ hs_m)
have hst_m : MeasurableSet[m] (s ∩ t) := (hs _).mpr (hs_m₂.inter ht)
simp_rw [this, setIntegral_condExp hm₂ (hf_int.indicator (hm _ hs_m)) ht,
setIntegral_condExp hm (hf_int.indicator (hm _ hs_m)) hst_m, integral_indicator (hm _ hs_m),
Measure.restrict_restrict (hm _ hs_m), ← Set.inter_assoc, Set.inter_self]
