setIntegral_condKernel — Mathlib

English

Let f be measurable, a, and a measurable set s; the iterated integral of f over s and the conditional kernel equals the integral of f over s×Ω with κ a.

Русский

Пусть f измерим, а и измеримое множество s; итерационный интеграл f над s и условного ядра равен интегралу f над s×Ω по κ a.

LaTeX

$$$\\int b\\in s, \\int ω, f(b,ω) \\; d( Kernel.condKernel (a,b) ) \\; d( Kernel.fst a ) = \\int x\\in s×Ω, f(x) \\; d( κ a )$$$

Lean4

theorem setIntegral_condKernel (a : α) {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t)
    (hf : IntegrableOn f (s ×ˢ t) (κ a)) :
    ∫ 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 [← κ.disintegrate κ.condKernel] at hf
  rw [setIntegral_compProd hs ht hf]

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