compProd_eq_sum_compProd — Mathlib

English

The kernel product κ ⊗ η equals the double indexed sum over n and m of seq κ n ⊗ seq η m.

Русский

Произведение ядер κ ⊗ η равно двойному суммированию над n и m: ∑_n ∑_m (seq κ n) ⊗ seq η m.

LaTeX

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

Lean4

theorem compProd_eq_sum_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] :
    κ ⊗ₖ η = Kernel.sum fun n ↦ Kernel.sum fun m ↦ seq κ n ⊗ₖ seq η m := by
  simp_rw [← compProd_eq_sum_compProd_right, ← compProd_eq_sum_compProd_left]

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