setLIntegral_condKernel_univ_right

English

A comprehensive formulation of the disintegration identity for measurable f: the iterated L-integral over fst and the conditional kernel equals the L-integral over the joint measure κ a.

Русский

Полная формула разложения плотности: итеративный L-интеграл по fst и условному ядру равен L-интегралу по совместной мере κ a.

LaTeX

$$$\\forall a\\; f,\\; \\mathrm{Measurable}(f) \\Rightarrow \\int b, \\int ω, f(b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = \\int x, f x ∂(κ a)$$$

Lean4

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

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