English
For a countable index κ_i of kernels, the density of the sum equals the sum of the densities: withDensity (Kernel.sum κ) f = Kernel.sum (λ i, (κ i).withDensity f).
Русский
Для счетного множителя ядер κ_i плотность суммы равна сумме плотностей: withDensity (Kernel.sum κ) f = Kernel.sum (λ i, (κ i).withDensity f).
LaTeX
$$$ \text{withDensity } (\text{Kernel.sum } κ) f = \text{Kernel.sum } (\lambda i, (κ i).withDensity f) $$$
Lean4
theorem withDensity_kernel_sum [Countable ι] (κ : ι → Kernel α β) (hκ : ∀ i, IsSFiniteKernel (κ i)) (f : α → β → ℝ≥0∞) :
withDensity (Kernel.sum κ) f = Kernel.sum fun i => withDensity (κ i) f :=
by
by_cases hf : Measurable (Function.uncurry f)
· ext1 a
simp_rw [sum_apply, Kernel.withDensity_apply _ hf, sum_apply, withDensity_sum (fun n => κ n a) (f a)]
· simp_rw [withDensity_of_not_measurable _ hf]
exact sum_zero.symm
