compProd_eq_sum_compProd_right — Mathlib

English

Dual to Left Sum, κ ⊗ η equals Kernel.sum over i of κ ⊗ seq η i, i.e., a right-hand decomposition into a sum of variable-structured kernels.

Русский

Двойственно слева: κ ⊗ η = ∑_i κ ⊗ seq η i, виртуально разложение правой части.

LaTeX

$$$$ \\kappa \\otimes_{\\kern-0.2em} \\eta = \\mathrm{Kernel.sum}\\ i \\; (\\kappa \\otimes_{\\kern-0.2em} (\\mathrm{seq}\\, \\eta\\, i)). $$$$

Lean4

theorem compProd_eq_sum_compProd_right (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel η] :
    κ ⊗ₖ η = Kernel.sum fun n => κ ⊗ₖ seq η n :=
  by
  simp_rw [compProd_def]
  rw [← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_left, ← comp_sum_right, ← parallelComp_sum_left,
    kernel_sum_seq]

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