condExp_mul_of_aestronglyMeasurable_left

English

If f is AEStronglyMeasurable and g is integrable, then CondExp of f·g equals f times CondExp g (aestronglyMeasurable variant).

Русский

Если f — AEStronglyMeasurable, g интегрируем, CondExp(f·g) = f·CondExp(g) в AES-тождестве.

LaTeX

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

Lean4

/-- Pull-out property of the conditional expectation. -/
theorem condExp_mul_of_aestronglyMeasurable_left {f g : α → ℝ} (hf : AEStronglyMeasurable[m] f μ)
    (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : μ[f * g|m] =ᵐ[μ] f * μ[g|m] :=
  by
  have : μ[f * g|m] =ᵐ[μ] μ[hf.mk f * g|m] := condExp_congr_ae (hf.ae_eq_mk.mul EventuallyEq.rfl)
  refine this.trans ?_
  have : f * μ[g|m] =ᵐ[μ] hf.mk f * μ[g|m] := hf.ae_eq_mk.mul EventuallyEq.rfl
  refine (condExp_mul_of_stronglyMeasurable_left hf.stronglyMeasurable_mk ?_ hg).trans this.symm
  refine (integrable_congr ?_).mp hfg
  exact hf.ae_eq_mk.mul EventuallyEq.rfl

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