English
The posterior operator is an involution up to μ-almost everywhere equality: applying posterior twice yields the original kernel.
Русский
Апостериорная операция является инволюцией до μ-нестрогого равенства: применение апостериорного оператора два раза даёт исходное ядро.
LaTeX
$$$ (\kappa^{\dagger}\mu)^{\dagger} (\kappa \circ_m \mu) =_{\mu\text{-a.e.}} \kappa $$$
Lean4
/-- The posterior is involutive (up to `μ`-a.e. equality). -/
theorem posterior_posterior [IsMarkovKernel κ] : (κ†μ)†(κ ∘ₘ μ) =ᵐ[μ] κ :=
by
suffices κ =ᵐ[κ†μ ∘ₘ κ ∘ₘ μ] (κ†μ)†(κ ∘ₘ μ)
by
rw [posterior_comp_self] at this
filter_upwards [this] with a h using h.symm
refine ae_eq_posterior_of_compProd_eq_swap_comp κ ?_
rw [posterior_comp_self, compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]
