English
If ι is countable and every κs(n) is IsSFiniteKernel, then Kernel.sum κs is IsSFiniteKernel.
Русский
Если ι счётно, и каждое κs(n) является IsSFiniteKernel, тогда Kernel.sum κs is IsSFiniteKernel.
LaTeX
$$$IsSFiniteKernel\\left(\\Kernel.sum \\kappa_s\\right).$$$
Lean4
instance isSFiniteKernel_sum [Countable ι] {κs : ι → Kernel α β} [hκs : ∀ n, IsSFiniteKernel (κs n)] :
IsSFiniteKernel (Kernel.sum κs) := by
cases fintypeOrInfinite ι
· rw [sum_fintype]
exact IsSFiniteKernel.finset_sum Finset.univ fun i _ => hκs i
cases nonempty_denumerable ι
exact isSFiniteKernel_sum_of_denumerable hκs