setIntegral_condKernel_univ_right

English

Under a monotone seq with union univ, densityProcess along seq m tends to densityProcess at univ, almost surely in x.

Русский

При монотонной последовательности с объединением univ плотность вдоль seq m стремится к плотности на univ почти для всех x.

LaTeX

$$$\\operatorname{Tendsto}\\left(m \\mapsto \\densityProcess κ (fst κ) n a x (seq m)\\right)\\_{\\operatorname{atTop}} (\\mathcal{NH}(\\densityProcess κ (fst κ) n a x univ))$$

Lean4

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

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