Pointwise finite kernels

A kernel whose measures are individually finite is s-finite, even when their total masses have no uniform bound. Normalizing by one plus the total mass gives a bounded kernel; the original kernel is recovered by a finite measurable density. Kernel.normalize also applies to arbitrary kernels, sending infinite-mass slices to zero, so it can be used with families that are only almost everywhere finite. This allows the parametric integration API to apply to random finite measures without artificial deterministic bounds.

noncomputable def ProbabilityTheory.Kernel.normalize {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : Kernel α β

Rescale each slice by one plus its total mass to obtain a kernel of mass at most one. Infinite-mass slices become zero; this is not normalization to a probability kernel.

@[simp]

theorem ProbabilityTheory.Kernel.normalize_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (a : α) : κ.normalize a = (1 + (κ a) Set.univ)⁻¹ • κ a

The slices of the normalized kernel.

instance ProbabilityTheory.Kernel.instIsFiniteKernelNormalize {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) : IsFiniteKernel κ.normalize

@[simp]

theorem ProbabilityTheory.Kernel.withDensity_normalize {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)] : (κ.normalize.withDensity fun (a : α) (x : β) => 1 + (κ a) Set.univ) = κ

Recover a pointwise finite kernel from its normalization by a measurable density.

theorem ProbabilityTheory.Kernel.isSFiniteKernel_of_isFiniteMeasure {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) [∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)] : IsSFiniteKernel κ

A pointwise finite kernel is s-finite. Uniform boundedness of the masses is unnecessary.