English
A lemma equating the conditional expectation of an indicator-modified function with the indicator-modified conditional expectation under suitable measurability assumptions.
Русский
Лемма, устанавливающая равенство CondExp для функции, умноженной на индикатор, и индикатор CondExp, при разумных предположениях о измеримости.
LaTeX
$$$$ \\mathrm{condExpIndicatorAux}(hs, hf) : \\mu[s.indicator f|m] =_{μ} s.indicator( \\mu[f|m] ) $$$$
Lean4
/-- The conditional expectation of the indicator of a function over an `m`-measurable set with
respect to the σ-algebra `m` is a.e. equal to the indicator of the conditional expectation. -/
theorem condExp_indicator (hf_int : Integrable f μ) (hs : MeasurableSet[m] s) :
μ[s.indicator f|m] =ᵐ[μ] s.indicator (μ[f|m]) :=
by
by_cases hm : m ≤ m0
swap; · simp_rw [condExp_of_not_le hm, Set.indicator_zero']; rfl
by_cases hμm : SigmaFinite (μ.trim hm)
swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm, Set.indicator_zero']; rfl
haveI : SigmaFinite (μ.trim hm) := hμm
have : s.indicator (μ[f|m]) =ᵐ[μ] s.indicator (μ[s.indicator f + sᶜ.indicator f|m]) := by
rw [Set.indicator_self_add_compl s f]
refine (this.trans ?_).symm
calc
s.indicator (μ[s.indicator f + sᶜ.indicator f|m]) =ᵐ[μ] s.indicator (μ[s.indicator f|m] + μ[sᶜ.indicator f|m]) :=
by
filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m] with x hx
classical rw [Set.indicator_apply, Set.indicator_apply, hx]
_ = s.indicator (μ[s.indicator f|m]) + s.indicator (μ[sᶜ.indicator f|m]) := (s.indicator_add' _ _)
_ =ᵐ[μ] s.indicator (μ[s.indicator f|m]) + s.indicator (sᶜ.indicator (μ[sᶜ.indicator f|m])) :=
by
refine Filter.EventuallyEq.rfl.add ?_
have : sᶜ.indicator (μ[sᶜ.indicator f|m]) =ᵐ[μ] μ[sᶜ.indicator f|m] :=
by
refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
· exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
· rw [Set.indicator_indicator, Set.inter_self]
filter_upwards [this] with x hx
by_cases hxs : x ∈ s
· simp only [hx, hxs, Set.indicator_of_mem]
· simp only [hxs, Set.indicator_of_notMem, not_false_iff]
_ =ᵐ[μ] s.indicator (μ[s.indicator f|m]) := by
rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
_ =ᵐ[μ] μ[s.indicator f|m] := by
refine (condExp_indicator_aux hs ?_).symm.trans ?_
· exact indicator_ae_eq_restrict_compl (hm _ hs)
· rw [Set.indicator_indicator, Set.inter_self]
