English
If f is integrable and s is measurable, then the conditional expectation of the indicator-modulated function equals the indicator of the conditional expectation of f.
Русский
Если f интегрируем и s измеримо, то CondExp индикатора f на s равен индикатору CondExp f.
LaTeX
$$$$ \\mu[f|m] \\mathbf{1}_s =_{a.e.} \\mathbf{1}_s \\mu[f|m] $$$$
Lean4
theorem condExp_restrict_ae_eq_restrict (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (hs_m : MeasurableSet[m] s)
(hf_int : Integrable f μ) : (μ.restrict s)[f|m] =ᵐ[μ.restrict s] μ[f|m] :=
by
have : SigmaFinite ((μ.restrict s).trim hm) := by rw [← restrict_trim hm _ hs_m]; infer_instance
rw [ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)]
refine EventuallyEq.trans ?_ (condExp_indicator hf_int hs_m)
refine ae_eq_condExp_of_forall_setIntegral_eq hm (hf_int.indicator (hm _ hs_m)) ?_ ?_ ?_
· intro t ht _
rw [← integrable_indicator_iff (hm _ ht), Set.indicator_indicator, Set.inter_comm, ← Set.indicator_indicator]
suffices h_int_restrict : Integrable (t.indicator ((μ.restrict s)[f|m])) (μ.restrict s)
by
rw [integrable_indicator_iff (hm _ hs_m), IntegrableOn]
exact h_int_restrict
exact integrable_condExp.indicator (hm _ ht)
· intro t ht _
calc
∫ x in t, s.indicator ((μ.restrict s)[f|m]) x ∂μ = ∫ x in t, ((μ.restrict s)[f|m]) x ∂μ.restrict s := by
rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m), Measure.restrict_restrict (hm _ ht),
Set.inter_comm]
_ = ∫ x in t, f x ∂μ.restrict s := (setIntegral_condExp hm hf_int.integrableOn ht)
_ = ∫ x in t, s.indicator f x ∂μ := by
rw [integral_indicator (hm _ hs_m), Measure.restrict_restrict (hm _ hs_m), Measure.restrict_restrict (hm _ ht),
Set.inter_comm]
· exact (stronglyMeasurable_condExp.indicator hs_m).aestronglyMeasurable
