posterior_id — Mathlib

English

The posterior of the identity kernel is the identity kernel almost surely.

Русский

Постериор идентичного ядра равен идентичному ядру почти наверняка.

LaTeX

$$$\\text{posterior}(Id, μ) =^{ae}_{μ} Id$$$

Lean4

/-- The posterior of the identity kernel is the identity kernel. -/
theorem posterior_id (μ : Measure Ω) [IsFiniteMeasure μ] : Kernel.id†μ =ᵐ[μ] Kernel.id :=
  by
  suffices Kernel.id =ᵐ[Kernel.id ∘ₘ μ] (Kernel.id : Kernel Ω Ω)†μ
    by
    rw [Measure.id_comp] at this
    filter_upwards [this] with a ha using ha.symm
  refine ae_eq_posterior_of_compProd_eq_swap_comp Kernel.id ?_
  rw [Measure.id_comp, Measure.compProd_id_eq_copy_comp, Measure.comp_assoc, Kernel.swap_copy]

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