lintegral_condKernel — Mathlib

English

For a fixed a and measurable s, the L-integral over s of the conditional kernel on the full Ω equals the measure of s×Ω under κ a.

Русский

Для данного a и измеримого s интеграл по s условного ядра на всё Ω равен мере множества s×Ω по κ a.

LaTeX

$$$\\int_{b\\in s} κ(a,b,\\Omega) \\, db = κ a(s\\times\\Omega)$$$

Lean4

theorem lintegral_condKernel (hf : Measurable f) (a : α) :
    ∫⁻ b, ∫⁻ ω, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = ∫⁻ x, f x ∂(κ a) :=
  by
  conv_rhs => rw [← κ.disintegrate κ.condKernel]
  rw [Kernel.lintegral_compProd _ _ _ hf]

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