English
If ι is denumerable and every κs(n) is IsSFiniteKernel, then Kernel.sum κs is IsSFiniteKernel.
Русский
Если ι денумерируемо и для каждого n ядро κs(n) является IsSFiniteKernel, то суммарное ядро Kernel.sum κs является IsSFiniteKernel.
LaTeX
$$$IsSFiniteKernel\\left(\\Kernel.sum \\kappa_s\\right).$$$
Lean4
theorem isSFiniteKernel_sum_of_denumerable [Denumerable ι] {κs : ι → Kernel α β} (hκs : ∀ n, IsSFiniteKernel (κs n)) :
IsSFiniteKernel (Kernel.sum κs) :=
by
let e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
refine ⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, ?_⟩⟩
have hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (seq (κs n)) := by simp_rw [kernel_sum_seq]
ext a s hs
rw [hκ_eq]
simp_rw [Kernel.sum_apply' _ _ hs]
change (∑' i, ∑' m, seq (κs i) m a s) = ∑' n, (fun im : ι × ℕ => seq (κs im.fst) im.snd a s) (e n)
rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s), ENNReal.summable.tsum_prod' fun _ => ENNReal.summable]
