ae_eq_posterior_of_compProd_eq_swap_comp

English

An equivalence transfers ae equality from compProd_posterior_eq_map_swap to ae equality of posteriors after swapping.

Русский

Эквивалентность переходит через ae равенство compProd_posterior_eq_map_swap к ae равенству постериоров после обмена.

LaTeX

$$$\\text{ae}(μ) \\quad \\Rightarrow \\quad η =^{ae}_{κ ∘ μ} κ†μ$$$

Lean4

/-- The posterior is unique up to a `κ ∘ₘ μ`-null set. -/
theorem ae_eq_posterior_of_compProd_eq_swap_comp (η : Kernel 𝓧 Ω) [IsFiniteKernel η]
    (h : ((κ ∘ₘ μ) ⊗ₘ η) = Kernel.swap Ω 𝓧 ∘ₘ μ ⊗ₘ κ) : η =ᵐ[κ ∘ₘ μ] κ†μ :=
  ae_eq_posterior_of_compProd_eq <| by rw [h, Measure.swap_comp]

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