Integration and kernel normalization

Integrals against a finite slice of a kernel can be recovered from integrals against its normalization by multiplying by one plus the slice's total mass. Only the chosen slice needs to be finite; the kernel need not have uniformly bounded masses or even be s-finite. These identities let finite-kernel integration results apply to individually finite slices.

theorem ProbabilityTheory.Kernel.lintegral_eq_mul_normalize {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (κ : Kernel α β) {a : α} (ha : (κ a) Set.univ ≠ ⊤) (f : β → ENNReal) : ∫⁻ (x : β), f x ∂κ a = (1 + (κ a) Set.univ) * ∫⁻ (x : β), f x ∂κ.normalize a

Recover a nonnegative integral from the normalized kernel at a finite slice.

theorem ProbabilityTheory.Kernel.integral_eq_smul_normalize {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (κ : Kernel α β) {a : α} (ha : (κ a) Set.univ ≠ ⊤) (f : β → F) : ∫ (x : β), f x ∂κ a = (1 + (κ a) Set.univ).toReal • ∫ (x : β), f x ∂κ.normalize a

Recover a Bochner integral from the normalized kernel at a finite slice. No integrability or completeness assumption is needed.