compProd_sum_right — Mathlib

English

For a family κ_i of kernels over a countable index set, μ ⊗ₘ (Kernel.sum κ) = sum_i (μ ⊗ₘ κ_i).

Русский

Для семейства ядров κ_i по сквозному индексу: μ ⊗ₘ (Kernel.sum κ) = ∑ μ ⊗ₘ κ_i.

LaTeX

$$$μ ⊗ₘ (Kernel.sum κ) = \\sum_i (μ ⊗ₘ κ_i)$$$

Lean4

theorem compProd_sum_right {ι : Type*} [Countable ι] {κ : ι → Kernel α β} [h : ∀ i, IsSFiniteKernel (κ i)] :
    μ ⊗ₘ (Kernel.sum κ) = sum (fun i ↦ μ ⊗ₘ (κ i)) :=
  by
  rw [compProd, ← Kernel.sum_prodMkLeft, Kernel.compProd_sum_right]
  rfl

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