setLIntegral_condKernel_univ_left

English

If f is measurable, the L-integral with κ, restricted to s and t, equals the L-integral over s×t of f with κ a.

Русский

Если f измерим, то L-интеграл с ограничением на s и t по κ равен L-интегралу по s×t с κ a.

LaTeX

$$$\\int_{b\\in s} \\int_{\\omega\\in t} f(b,\\omega) \\, d(\\Kernel.condKernel (a,b)) \\, d(\\Kernel.fst a) = \\int_{x\\in s\\times t} f(x) \\, d(κ a)$$$

Lean4

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

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