compProd_prodMkLeft_eq_comp — Mathlib

English

Associativity-like rule for parallel composition: (η ∥ η') ∘ (κ ∥ κ') = (η ∘ κ) ∥ (η' ∘ κ').

Русский

Асоциативное свойство параллельной композиции ядер.

LaTeX

$$$$ (η \\parallelκ η') \\circκ (κ' \\parallelκ κ'') = (η ∘ κ) \\parallelκ (η' ∘ κ') $$$$

Lean4

theorem compProd_prodMkLeft_eq_comp (κ : Kernel X Y) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η] :
    κ ⊗ₖ (prodMkLeft X η) = (Kernel.id ×ₖ η) ∘ₖ κ := by
  ext a s hs
  rw [comp_eq_snd_compProd, compProd_apply hs, snd_apply' _ _ hs, compProd_apply]
  swap; · exact measurable_snd hs
  simp only [prodMkLeft_apply, ← Set.preimage_comp, Prod.snd_comp_mk, Set.preimage_id_eq, id_eq, prod_apply' _ _ _ hs,
    id_apply]
  congr with b
  rw [lintegral_dirac']
  exact measurable_measure_prodMk_left hs

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