setIntegral_condKernel_univ_left — Mathlib

English

If f is measurable, and t is measurable, then the integral over the whole first coordinate with f restricted to univ×t equals the integral over univ×t of f with κ a.

Русский

Если f измеримо, и t измеримо, то интеграл по первой координате с f на univ×t равен интегралу по univ×t для κ a.

LaTeX

$$$\\int b, \\int ω in t, f(b,ω) \\, d(Kernel.condKernel (a,b)) \\, d(Kernel.fst a) = \\int x in (Set.univ × t), f(x) \\, d(κ a)$$$

Lean4

theorem setIntegral_condKernel_univ_left (a : α) {t : Set Ω} (ht : MeasurableSet t)
    (hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)) :
    ∫ b, ∫ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = ∫ x in Set.univ ×ˢ t, f x ∂(κ a) := by
  rw [← setIntegral_condKernel a MeasurableSet.univ ht hf]; simp_rw [Measure.restrict_univ]

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