lintegral_snd — Mathlib

English

If κ is a Markov kernel, then snd κ is also a Markov kernel.

Русский

Если κ является ядром Маркова, то snd κ тоже является ядром Маркова.

LaTeX

$$$\\text{IsMarkovKernel}(κ) \\implies \\text{IsMarkovKernel}(snd(κ))$$$

Lean4

theorem lintegral_snd (κ : Kernel α (β × γ)) (a : α) {g : γ → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂snd κ a = ∫⁻ bc : β × γ, g bc.snd ∂κ a := by rw [snd_eq, lintegral_map _ measurable_snd a hg]

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