English
There exists an ℕ-indexed martingale densityProcess κ ν on α with respect to ν, describing the density of κ relative to ν over the sets given by the countable partitions of γ at level n.
Русский
Существует плотностной процесс densityProcess κ ν с индексом по натуральным числам, являющийся мартингалью относительно ν и задающий плотность κ по отношению к ν на множествах, образующих разбиения γ на уровне n.
LaTeX
$$$\text{densityProcess}(\kappa,\nu,n,a,x,s) = \left( \dfrac{\kappa a(\text{countablePartitionSet} n x \times^s s)}{\nu a(\text{countablePartitionSet} n x)} \right)^{\mathrm{toReal}}$$$
Lean4
/-- 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. -/
noncomputable def densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α) (x : γ) (s : Set β) : ℝ :=
(κ a (countablePartitionSet n x ×ˢ s) / ν a (countablePartitionSet n x)).toReal
