parallelComp_comp_compProd — Mathlib

English

Let κ be a finite kernel and η a finite kernel with η: Kernel β γ. Then (Kernel.id ∥ₖ η) ∘ₘ (μ ⊗ₘ κ) = μ ⊗ₘ (η ∘ₖ κ).

Русский

Пусть κ — конечное ядро, η — конечное ядро с η: Kernel β γ. Тогда (Kernel.id ∥ₖ η) ∘ₘ (μ ⊗ₘ κ) = μ ⊗ₘ (η ∘ₖ κ).

LaTeX

$$$$(\\text{Kernel.id} \\parallel_k \\eta) \\circ_m (\\mu \\otimes_m \\kappa) = \\mu \\otimes_m (\\eta \\circ_k \\kappa).$$$$

Lean4

theorem parallelComp_comp_compProd [IsSFiniteKernel κ] {η : Kernel β γ} [IsSFiniteKernel η] :
    (Kernel.id ∥ₖ η) ∘ₘ (μ ⊗ₘ κ) = μ ⊗ₘ (η ∘ₖ κ) :=
  by
  by_cases hμ : SFinite μ
  swap; · simp [hμ]
  rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc, Kernel.parallelComp_comp_prod,
    Kernel.id_comp]

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