integral_condDistrib_map — Mathlib

English

The conditional distribution is a Markov kernel; hence there is an instance of Markov kernel structure on condDistrib.

Русский

Условное распределение является ядром Маркова; следовательно, существует структура ядра Маркова на condDistrib.

LaTeX

$$$$\\mathrm{IsMarkovKernel}(\\mathrm{condDistrib}(Y,X,μ)).$$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂condDistrib Y X μ x) (μ.map X) := by
  rw [← Measure.fst_map_prodMk₀ hY, condDistrib]; exact hf.integral_condKernel

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