Radon-Nikodym derivative and Lebesgue decomposition for kernels #

Let γ be a countably generated measurable space and κ, η : kernel α γ be finite kernels. Then there exists a function kernel.rnDeriv κ η : α → γ → ℝ≥0∞ jointly measurable on α × γ and a kernel kernel.singularPart κ η : kernel α γ such that

κ = kernel.withDensity η (kernel.rnDeriv κ η) + kernel.singularPart κ η,
for all a : α, kernel.singularPart κ η a ⟂ₘ η a,
for all a : α, kernel.singularPart κ η a = 0 ↔ κ a ≪ η a,
for all a : α, kernel.withDensity η (kernel.rnDeriv κ η) a = 0 ↔ κ a ⟂ₘ η a.

Furthermore, the sets {a | κ a ≪ η a} and {a | κ a ⟂ₘ η a} are measurable.

The construction of the derivative starts from kernel.density: for two finite kernels κ' : kernel α (γ × β) and η' : kernel α γ with fst κ' ≤ η', the function density κ' η' : α → γ → Set β → ℝ is jointly measurable in the first two arguments and satisfies that for all a : α and all measurable sets s : Set β and A : Set γ, ∫ x in A, density κ' η' a x s ∂(η' a) = (κ' a (A ×ˢ s)).toReal. We use that definition for β = Unit and κ' = map κ (fun a ↦ (a, ())). We can't choose η' = η in general because we might not have κ ≤ η, but if we could, we would get a measurable function f with the property κ = withDensity η f, which is the decomposition we want for κ ≤ η. To circumvent that difficulty, we take η' = κ + η and thus define rnDerivAux κ η. Finally, rnDeriv κ η a x is given by ENNReal.ofReal (rnDerivAux κ (κ + η) a x) / ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a x). Up to some conversions between ℝ and ℝ≥0, the singular part is withDensity (κ + η) (rnDerivAux κ (κ + η) - (1 - rnDerivAux κ (κ + η)) * rnDeriv κ η).

The countably generated measurable space assumption is not needed to have a decomposition for measures, but the additional difficulty with kernels is to obtain joint measurability of the derivative. This is why we can't simply define rnDeriv κ η by a ↦ (κ a).rnDeriv (ν a) everywhere (although rnDeriv κ η has that value almost everywhere). See the construction of kernel.density for details on how the countably generated hypothesis is used.

Main definitions #

ProbabilityTheory.kernel.rnDeriv: a function α → γ → ℝ≥0∞ jointly measurable on α × γ
ProbabilityTheory.kernel.singularPart: a kernel α γ

Main statements #

ProbabilityTheory.kernel.mutuallySingular_singularPart: for all a : α, kernel.singularPart κ η a ⟂ₘ η a
ProbabilityTheory.kernel.rnDeriv_add_singularPart: kernel.withDensity η (kernel.rnDeriv κ η) + kernel.singularPart κ η = κ
ProbabilityTheory.kernel.measurableSet_absolutelyContinuous : the set {a | κ a ≪ η a} is Measurable
ProbabilityTheory.kernel.measurableSet_mutuallySingular : the set {a | κ a ⟂ₘ η a} is Measurable

References #

Theorem 1.28 in [O. Kallenberg, Random Measures, Theory and Applications][kallenberg2017].

TODO #

prove uniqueness results.
link kernel Radon-Nikodym derivative and Radon-Nikodym derivative of measures, and similarly for singular parts.