setIntegral_condKernel — Mathlib

English

For measurable sets s in β and t in Ω, the integral over s×t equals the restricted integral over ρ.

Русский

Для измеримых множеств s⊂β и t⊂Ω утверждается равенство интегралов над s×t и над соответствующим ограниченным множеством меры ρ.

LaTeX

$$$\\int b \\in s, \\int \\omega \\in t \\, f(b,\\omega) \\, d(\\rho.condKernel b) \\, d\\rho.fst = \\int x \\in s \\times\\! t \\, f(x) \\, d\\rho$$$

Lean4

theorem setIntegral_condKernel {s : Set β} (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t)
    (hf : IntegrableOn f (s ×ˢ t) ρ) : ∫ b in s, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ :=
  by
  conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  rw [← ρ.disintegrate ρ.condKernel] at hf
  rw [setIntegral_compProd hs ht hf]

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