posterior_comp_self — Mathlib

English

If κ is deterministic with respect to Ω → 𝓧, then κ ∘ₖ κ†μ is almost surely equal to μ.map f, where f is the representing function.

Русский

Если κ детерминированно зависимо от тождественного отображения, то κ ∘ₖ κ†μ равносильно μ.map f почти наверняка.

LaTeX

$$$\\text{deterministic}(f) \\Rightarrow κ ∘ₖ κ†μ =^{ae}_{μ.map f} μ.map f$$$

Lean4

@[simp]
theorem posterior_comp_self [IsMarkovKernel κ] : κ†μ ∘ₘ κ ∘ₘ μ = μ := by
  rw [← Measure.snd_compProd, compProd_posterior_eq_map_swap, Measure.snd_map_swap, Measure.fst_compProd]

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