setLIntegral_condKernel_univ_right

English

For a fixed a, the left-hand L-integral over all b of the conditional kernel on univ in Ω equals the right-hand L-integral over univ in Ω of the kernel a.

Русский

Для данного a лево-правый L-интеграл по всем b условного ядра на univ в Ω равен правому L-интегралу по univ в Ω ядра a.

LaTeX

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

Lean4

theorem setLIntegral_condKernel_univ_right (hf : Measurable f) (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ b in s, ∫⁻ ω, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = ∫⁻ x in s ×ˢ Set.univ, f x ∂(κ a) := by
  rw [← setLIntegral_condKernel hf a hs MeasurableSet.univ]; simp_rw [Measure.restrict_univ]

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