English
If κ is s-finite and f: α→β→ NNReal, then κ.withDensity (ENNReal.ofNNReal ∘ f) is s-finite.
Русский
Если κ является s-финитным и f: α→β→ NNReal, то κ.withDensity(ENNReal.ofNNReal ∘ f) является s-финитным.
LaTeX
$$$\\operatorname{IsSFiniteKernel}\\Bigl(\\mathrm{withDensity}\\,\\kappa\\; (\\lambda a b. \\mathrm{ENNReal.ofNNReal}(f(a,b)))\\Bigr)$$$
Lean4
/-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0∞` which is everywhere finite,
`withDensity κ f` is s-finite. -/
nonrec theorem withDensity (κ : Kernel α β) [IsSFiniteKernel κ] (hf_ne_top : ∀ a b, f a b ≠ ∞) :
IsSFiniteKernel (withDensity κ f) :=
by
have h_eq_sum : withDensity κ f = Kernel.sum fun i => withDensity (seq κ i) f :=
by
rw [← withDensity_kernel_sum _ _]
congr
exact (kernel_sum_seq κ).symm
rw [h_eq_sum]
exact isSFiniteKernel_sum (hκs := fun n => isSFiniteKernel_withDensity_of_isFiniteKernel (seq κ n) hf_ne_top)
