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]