Kernel density #

Let κ : Kernel α (γ × β) and ν : Kernel α γ be two finite kernels with Kernel.fst κ ≤ ν, where γ has a countably generated σ-algebra (true in particular for standard Borel spaces). We build a function density κ ν : α → γ → Set β → ℝ jointly measurable in the first two arguments such that for all a : α and all measurable sets s : Set β and A : Set γ, ∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s).

There are two main applications of this construction.

Disintegration of kernels: for κ : Kernel α (γ × β), we want to build a kernel η : Kernel (α × γ) β such that κ = fst κ ⊗ₖ η. For β = ℝ, we can use the density of κ with respect to fst κ for intervals to build a kernel cumulative distribution function for η. The construction can then be extended to β standard Borel.
Radon-Nikodym theorem for kernels: for κ ν : Kernel α γ, we can use the density to build a Radon-Nikodym derivative of κ with respect to ν. We don't need β here but we can apply the density construction to β = Unit. The derivative construction will use density but will not be exactly equal to it because we will want to remove the fst κ ≤ ν assumption.

Main definitions #

ProbabilityTheory.Kernel.density: for κ : Kernel α (γ × β) and ν : Kernel α γ two finite kernels, Kernel.density κ ν is a function α → γ → Set β → ℝ.

Main statements #

ProbabilityTheory.Kernel.setIntegral_density: for all measurable sets A : Set γ and s : Set β, ∫ x in A, Kernel.density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s).
ProbabilityTheory.Kernel.measurable_density: the function p : α × γ ↦ Kernel.density κ ν p.1 p.2 s is measurable.

Construction of the density #

If we were interested only in a fixed a : α, then we could use the Radon-Nikodym derivative to build the density function density κ ν, as follows.

def density' (κ : Kernel α (γ × β)) (ν : kernel a γ) (a : α) (x : γ) (s : Set β) : ℝ :=
  (((κ a).restrict (univ ×ˢ s)).fst.rnDeriv (ν a) x).toReal

However, we can't turn those functions for each a into a measurable function of the pair (a, x).

In order to obtain measurability through countability, we use the fact that the measurable space γ is countably generated. For each n : ℕ, we define (in the file Mathlib/Probability/Process/PartitionFiltration.lean) a finite partition of γ, such that those partitions are finer as n grows, and the σ-algebra generated by the union of all partitions is the σ-algebra of γ. For x : γ, countablePartitionSet n x denotes the set in the partition such that x ∈ countablePartitionSet n x.

For a given n, the function densityProcess κ ν n : α → γ → Set β → ℝ defined by fun a x s ↦ (κ a (countablePartitionSet n x ×ˢ s) / ν a (countablePartitionSet n x)).toReal has the desired property that ∫ x in A, densityProcess κ ν n a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal for all A in the σ-algebra generated by the partition at scale n and is measurable in (a, x).

countableFiltration γ is the filtration of those σ-algebras for all n : ℕ. The functions densityProcess κ ν n described here are a bounded ν-martingale for the filtration countableFiltration γ. By Doob's martingale L1 convergence theorem, that martingale converges to a limit, which has a product-measurable version and satisfies the integral equality for all A in ⨆ n, countableFiltration γ n. Finally, the partitions were chosen such that that supremum is equal to the σ-algebra on γ, hence the equality holds for all measurable sets. We have obtained the desired density function.

References #

The construction of the density process in this file follows the proof of Theorem 9.27 in [O. Kallenberg, Foundations of modern probability][kallenberg2021], adapted to use a countably generated hypothesis instead of specializing to ℝ.