instIsSFiniteKernelWithDensityOfNNReal

English

For an s-finite kernel κ and a NNReal-valued function f, κ.withDensity (λ a b, ENNReal.ofNNReal (f a b)) is s-finite.

Русский

Для s-финитного ядра κ и функции, принимающей значения NNReal, κ.withDensity(λ a b, ENNReal.ofNNReal (f a b)) является s-финитным.

LaTeX

$$$\\operatorname{IsSFiniteKernel}\\bigl(\\mathrm{withDensity}(\\kappa, \\lambda a b. ENNReal.ofNNReal (f(a,b)))\\bigr)$$$

Lean4

/-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0`, `withDensity κ f` is s-finite. -/
instance (κ : Kernel α β) [IsSFiniteKernel κ] (f : α → β → ℝ≥0) : IsSFiniteKernel (withDensity κ fun a b => f a b) :=
  IsSFiniteKernel.withDensity κ fun _ _ => ENNReal.coe_ne_top

Похожие утверждения