condExp_indicator_aux — Mathlib

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

Похожие утверждения