English
Let η be a kernel from 𝓧 to 𝓨. Then the posterior of κ with respect to μ composed with η is, in a precise sense, the same as applying η after taking the posterior of κ with μ. This expresses a contravariance property of the posterior transformation.
Русский
Пусть η — ядро 𝓧 → 𝓨. Тогда постериорная операция над κ относительно μ, затем над η, равна применению η после постериора κ относительно μ (формально в смысле почти всеезависимости). Это выражает противо-детерминированность постериорной трансформации.
LaTeX
$$$$(\eta \circ_k \kappa)^{\dagger}\mu =_{a.e.}^{\, (\eta \circ_m \kappa \circ_m \mu)} \kappa^{\dagger}\mu \circ_k \eta^{\dagger}(\kappa \circ_m \mu).$$$$
Lean4
/-- The posterior is contravariant. -/
theorem posterior_comp {η : Kernel 𝓧 𝓨} [IsFiniteKernel η] : (η ∘ₖ κ)†μ =ᵐ[η ∘ₘ κ ∘ₘ μ] κ†μ ∘ₖ η†(κ ∘ₘ μ) :=
by
rw [Measure.comp_assoc]
refine (ae_eq_posterior_of_compProd_eq_swap_comp ((κ†μ) ∘ₖ η†(κ ∘ₘ μ)) ?_).symm
simp_rw [Measure.compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, ←
Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
calc
(Kernel.id ∥ₖ κ†μ) ∘ₘ (Kernel.id ∥ₖ η†(κ ∘ₘ μ)) ∘ₘ (Kernel.copy 𝓨) ∘ₘ η ∘ₘ κ ∘ₘ μ
_ = (Kernel.id ∥ₖ κ†μ) ∘ₘ (η ∥ₖ Kernel.id) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
rw [parallelProd_posterior_comp_copy_comp]
_ = (η ∥ₖ Kernel.id) ∘ₘ (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]
_ = (η ∥ₖ Kernel.id) ∘ₘ (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by rw [parallelProd_posterior_comp_copy_comp]
_ = (Kernel.swap _ _) ∘ₘ (Kernel.id ∥ₖ η) ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ :=
by
simp_rw [Measure.comp_assoc]
conv_rhs => rw [← Kernel.comp_assoc]
rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧), Kernel.swap_parallelComp,
Kernel.comp_assoc, Kernel.swap_copy]
