English
If f is strongly measurable and g is integrable, then the conditional expectation of the product f · g equals f times the conditional expectation of g (on the left).
Русский
Если f сильно измеримо, а g интегрируем, то CondExp(f·g) = f · CondExp(g) слева.
LaTeX
$$$$ \\mu[f \\cdot g|m] =_{a.e.} f \\cdot \\mu[g|m] $$$$
Lean4
/-- Auxiliary lemma for `condExp_indicator`. -/
theorem condExp_indicator_aux (hs : MeasurableSet[m] s) (hf : f =ᵐ[μ.restrict sᶜ] 0) :
μ[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
have hsf_zero : ∀ g : α → E, g =ᵐ[μ.restrict sᶜ] 0 → s.indicator g =ᵐ[μ] g := fun g =>
indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs)
refine ((hsf_zero (μ[f|m]) (condExp_ae_eq_restrict_zero hs.compl hf)).trans ?_).symm
exact condExp_congr_ae (hsf_zero f hf).symm