English
Parallel composition is compatible with swapping copies: (swap ∘ parallel) = (parallel ∘ swap).
Русский
Композиция параллельности совместима с перестановками копий.
LaTeX
$$$$ swap \\circ (\\kappa \\parallel κ') = (κ' \\parallel κ) \\circ swap $$$$
Lean4
theorem parallelComp_id_left_comp_parallelComp {η : Kernel X' Z} [IsSFiniteKernel η] {ξ : Kernel Z T}
[IsSFiniteKernel ξ] : (Kernel.id ∥ₖ ξ) ∘ₖ (κ ∥ₖ η) = κ ∥ₖ (ξ ∘ₖ η) :=
by
by_cases hκ : IsSFiniteKernel κ
swap; · simp [hκ]
ext a s hs
rw [comp_apply' _ _ _ hs, parallelComp_apply,
MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]
rw [parallelComp_apply, Measure.prod_apply hs]
congr with x
rw [comp_apply' _ _ _ (measurable_prodMk_left hs)]
congr with y
rw [parallelComp_apply' hs, Kernel.id_apply, lintegral_dirac' _ (measurable_measure_prodMk_left hs)]