English
Let κ: γ→β, η: ε→β′, ξ: (ε×β)→δ, f γ→ε deterministic. Then (ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) equals (ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf).
Русский
Пусть κ: γ→β, η: ε→β′, ξ: (ε×β)→δ, f детерминирован. Тогда (ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) равно (ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf).
LaTeX
$$$$(\\xi ×_k η.{\\text{prodMkRight } β}) ∘_k (deterministic f hf ×_k κ) = (\\xi ∘_k (deterministic f hf ×_k κ)) ×_k (\\eta ∘_k deterministic f hf).$$$$
Lean4
theorem prod_comp_left [SFinite μ] [SFinite ν] {κ : Kernel α γ} [IsSFiniteKernel κ] :
(κ ∘ₘ μ).prod ν = (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) :=
by
have h1 : (κ ∘ₘ μ).prod ν = (ν.prod (κ ∘ₘ μ)).map Prod.swap := by rw [Measure.prod_swap]
have h2 : (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
calc
(κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
_ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
_ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
rw [Kernel.swap, Measure.deterministic_comp_eq_map]
_ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
_ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by rw [Kernel.swap, Measure.deterministic_comp_eq_map]
rw [← Measure.prod_comp_right, ← h1] at h2
exact h2.symm
