Commit 2024-03-27 15:04 4e40a0d0

feat: Radon-Nikodym theorem for transition kernels (#10950) Let γ be a countably generated measurable space and κ η : kernel α γ be finite kernels. We build a function rnDeriv κ η : α → γ → ℝ≥0∞ jointly measurable on α × γ and a kernel singularPart κ η : kernel α γ such that κ = withDensity η (rnDeriv κ η) + singularPart κ η and for all a : α, singularPart κ η a ⟂ₘ η a .