setLIntegral_condKernel — Mathlib

English

A key formulation of the kernel disintegration: the left integral over s of the conditional kernel against t equals the measure of s×t under κ a.

Русский

Ключевое формулирование разложения ядра: левый интеграл по s условного ядра против t равен мере s×t по κ a.

LaTeX

$$$\\int_{b\\in s} κ(a,b,t) \\; d b = κ a(s\\times t)$$$

Lean4

theorem setLIntegral_condKernel (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set Ω}
    (ht : MeasurableSet t) :
    ∫⁻ b in s, ∫⁻ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = ∫⁻ x in s ×ˢ t, f x ∂(κ a) :=
  by
  conv_rhs => rw [← κ.disintegrate κ.condKernel]
  rw [Kernel.setLIntegral_compProd _ _ _ hf hs ht]

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