condExp_mul_of_aestronglyMeasurable_right

English

Symmetric variant: CondExp of f·g equals CondExp f times g when f is AEStronglyMeasurable and g integrable.

Русский

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

LaTeX

$$$$ \\mathrm{CondExp}_{m, \\mu}(f \\cdot g) = \\mathrm{CondExp}_{m, \\mu}(f) \\cdot g \\\\text{ a.e. } $$$$

Lean4

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

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