compProd_eq_tsum_compProd — Mathlib

English

The product kernel satisfies a tsum (infinite sum) decomposition: (κ ⊗ η) a s equals the double sum over n,m of (seq κ n ⊗ seq η m) a s.

Русский

Произведение ядер имеет разложение через бесконечную сумму: (κ ⊗ η) a s = ∑′_n ∑′_m (seq κ n ⊗ seq η m) a s.

LaTeX

$$$$ (\\kappa \\otimes_{\\kern-0.2em} \\eta) a\\; s = \\sum'_{n \\in \\mathbb{N}} \\sum'_{m \\in \\mathbb{N}} (\\mathrm{seq}\\, \\kappa\\, n \\otimes_{\\kern-0.2em} \\mathrm{seq}\\, \\eta\\, m) a\\; s. $$$$

Lean4

theorem compProd_eq_tsum_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η]
    (a : α) (hs : MeasurableSet s) : (κ ⊗ₖ η) a s = ∑' (n : ℕ) (m : ℕ), (seq κ n ⊗ₖ seq η m) a s :=
  by
  rw [compProd_eq_sum_compProd]
  simp_rw [sum_apply' _ _ hs]

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