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 (A ×ˢ s)).toReal
.
There are two main applications of this construction (still TODO, in other files).
- Disintegration of kernels: for
κ : Kernel α (γ × β)
, we want to build a kernelη : Kernel (α × γ) β
such thatκ = fst κ ⊗ₖ η
. Forβ = ℝ
, we can use the density ofκ
with respect tofst κ
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 usedensity
but will not be exactly equal to it because we will want to remove thefst κ ≤ ν
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 setsA : Set γ
ands : Set β
,∫ x in A, Kernel.density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal
.ProbabilityTheory.Kernel.measurable_density
: the functionp : α × γ ↦ 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
) 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 ℝ
.
An ℕ
-indexed martingale that is a density for κ
with respect to ν
on the sets in
countablePartition γ n
. Used to define its limit ProbabilityTheory.Kernel.density
, which is
a density for those kernels for all measurable sets.
Equations
- κ.densityProcess ν n a x s = ((κ a) (MeasurableSpace.countablePartitionSet n x ×ˢ s) / (ν a) (MeasurableSpace.countablePartitionSet n x)).toReal
Instances For
Alias of ProbabilityTheory.Kernel.eLpNorm_densityProcess_le
.
Alias of ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem
.
Alias of ProbabilityTheory.Kernel.setIntegral_densityProcess
.
Alias of ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le
.
Alias of ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess
.
Alias of ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess
.
Density of the kernel κ
with respect to ν
. This is a function α → γ → Set β → ℝ
which
is measurable on α × γ
for all measurable sets s : Set β
and satisfies that
∫ x in A, density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal
for all measurable A : Set γ
.
Equations
- κ.density ν a x s = Filter.limsup (fun (n : ℕ) => κ.densityProcess ν n a x s) Filter.atTop
Instances For
Alias of ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess
.
Auxiliary lemma for setIntegral_density
.
Alias of ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet
.
Auxiliary lemma for setIntegral_density
.
We specialize to ν = fst κ
, for which density κ (fst κ) a t univ = 1
almost everywhere.