integral_kernel_condKernel — Mathlib

English

Equality of iterated integrals against a kernel conditional on (a,b) with the joint integral against κ a, for appropriate f and measurability assumptions.

Русский

Сверка итерационных интегралов против условного ядра на (a,b) с совместной интеграцией по κ a.

LaTeX

$$$\\int b \\int \\omega f(b,\\omega) \\, d(Kernel.condKernel(a,b)) \\, d(κ a) = \\int x f(x) \\, d(κ a)$$$

Lean4

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

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