condExp_mul_of_stronglyMeasurable_right

English

Symmetric pull-out: CondExp of f·g equals CondExp f times g when g is strongly measurable and f integrable.

Русский

Симметричное выносное свойство: CondExp(f·g) = CondExp(f)·g при условии, что g сильно измеримо и f интегрируемо.

LaTeX

$$$$ \\mu[ f \\cdot g|m ] =_{a.e.} \\mu[f|m] \\cdot g, $$$$

Lean4

/-- Pull-out property of the conditional expectation. -/
theorem condExp_mul_of_stronglyMeasurable_right {f g : α → ℝ} (hg : StronglyMeasurable[m] g)
    (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : μ[f * g|m] =ᵐ[μ] μ[f|m] * g := by
  simpa [mul_comm] using condExp_mul_of_stronglyMeasurable_left hg (mul_comm f g ▸ hfg) hf

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