aestronglyMeasurable_trim_condExpKernel

English

On μ.trim hm, almost everywhere f equals its a.e.-class transported by condExpKernel, for any AEStronglyMeasurable f.

Русский

На μ.trim hm почти повсюду f равна своему эквиваленту по условному ядру condExpKernel, если f — AEStronglyMeasurable.

LaTeX

$$$\\forall\\text{almost every }ω\\;\\ (f =^ {a.e.}_{condExpKernel(μ,m,ω)} f)\\text{ на }μ.trim(hm)$$$

Lean4

theorem aestronglyMeasurable_trim_condExpKernel (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) :
    ∀ᵐ ω ∂(μ.trim hm), f =ᵐ[condExpKernel μ m ω] hf.mk f :=
  by
  refine Measure.ae_ae_of_ae_comp ?_
  rw [condExpKernel_comp_trim hm]
  exact hf.ae_eq_mk

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