integral_condKernel — Mathlib

English

Let f be AES-trongly measurable with respect to ρ. Then the map x ↦ ∫ f(x,y) dρ.condKernel(x) is AES-measurable with respect to ρ.fst.

Русский

Пусть f обладает AES-измеримостью относительно ρ. Тогда функция x ↦ ∫ f(x,y) dρ.condKernel(x) является AES-измеримой относительно ρ.fst.

LaTeX

$$$\\mathrm{AEStronglyMeasurable}(f,\\rho) \\Rightarrow \\mathrm{AEStronglyMeasurable}\\left( x \\mapsto \\int_y f(x,y) \\, \\partial\\rho.condKernel(x) \\right) \\; \\rho.fst$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condKernel (hf : AEStronglyMeasurable f ρ) :
    AEStronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂ρ.condKernel x) ρ.fst :=
  by
  rw [← ρ.disintegrate ρ.condKernel] at hf
  exact AEStronglyMeasurable.integral_kernel_compProd hf

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