English
Let I be a finite index set and κi a family of kernels α → β indexed by I. If every κi is IsSFiniteKernel, then the finite sum ∑i∈I κi is IsSFiniteKernel.
Русский
Пусть I — конечное Индексное множество и κ_i — семейство ядер α → β, индексированное по I. Если каждое κ_i является IsSFiniteKernel, то конечная сумма ∑_{i∈I} κ_i является IsSFiniteKernel.
LaTeX
$$$\\forall I \\in \\mathrm{Finset}(\\iota), \\bigl( \\forall i \\in I,\\ IsSFiniteKernel(\\kappa_i) \\bigr) \\Rightarrow IsSFiniteKernel\\left(\\sum_{i \\in I} \\kappa_i\\right).$$$
Lean4
theorem finset_sum {κs : ι → Kernel α β} (I : Finset ι) (h : ∀ i ∈ I, IsSFiniteKernel (κs i)) :
IsSFiniteKernel (∑ i ∈ I, κs i) := by
classical
induction I using Finset.induction with
| empty => rw [Finset.sum_empty]; infer_instance
| insert i I hi_notMem_I h_ind =>
rw [Finset.sum_insert hi_notMem_I]
haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
have : IsSFiniteKernel (∑ x ∈ I, κs x) := h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
exact IsSFiniteKernel.add _ _
