English
Parallel composition commuting with the standard composition via swapping identities yields the same product.
Русский
Параллельная композиция и стандартная композиция взаимно приводят к одинаковому произведению через перестановку.
LaTeX
$$$$ swap Y T \\circ (κ \\parallel κ') = (κ) \\parallel (κ') \\circ swap X Z $$$$
Lean4
theorem swap_parallelComp : swap Y T ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap X Z :=
by
by_cases hκ : IsSFiniteKernel κ
swap; · simp [hκ]
by_cases hη : IsSFiniteKernel η
swap; · simp [hη]
ext ac s hs
simp_rw [comp_apply, parallelComp_apply, Measure.bind_apply hs (Kernel.aemeasurable _), swap_apply,
lintegral_dirac' _ (Kernel.measurable_coe _ hs), parallelComp_apply' hs, Prod.fst_swap, Prod.snd_swap]
rw [MeasureTheory.lintegral_prod_symm]
swap; · exact ((Kernel.id.measurable_coe hs).comp measurable_swap).aemeasurable
congr with d
simp_rw [Prod.swap_prod_mk, Measure.dirac_apply' _ hs, ← Set.indicator_comp_right,
lintegral_indicator (measurable_prodMk_left hs)]
simp
