parallelComp_id_left_comp_parallelComp

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)]

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