condExp_stronglyMeasurable_mul_of_bound₀

English

If f is AEStronglyMeasurable and bounded, then the same Mul-bound CondExp identity holds with a zero-augmented anchor.

Русский

Если f — AEStronglyMeasurable и ограничено, то аналогичное тождество CondExp для умножения держится.

LaTeX

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

Lean4

theorem condExp_stronglyMeasurable_mul_of_bound₀ (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ}
    (hf : AEStronglyMeasurable[m] f μ) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
    μ[f * g|m] =ᵐ[μ] f * μ[g|m] := by
  grw [hf.ae_eq_mk]
  refine condExp_stronglyMeasurable_mul_of_bound hm hf.stronglyMeasurable_mk hg c ?_
  filter_upwards [hf_bound, hf.ae_eq_mk] with x hxc hx_eq
  rwa [← hx_eq]

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