English
For any kernels κ ≤ η, rnDerivAux κ η a x is nonnegative for all a,x (with the appropriate almost-everywhere interpretation).
Русский
Для любых ядер κ ≤ η rnDerivAux κ η a x неотрицателен (с соответствующей almost-everywhere интерпретацией).
LaTeX
$$$$ 0 \le rnDerivAux κ η a x.$$$$
Lean4
/-- Auxiliary function used to define `ProbabilityTheory.Kernel.rnDeriv` and
`ProbabilityTheory.Kernel.singularPart`.
This has the properties we want for a Radon-Nikodym derivative only if `κ ≪ ν`. The definition of
`rnDeriv κ η` will be built from `rnDerivAux κ (κ + η)`. -/
noncomputable def rnDerivAux (κ η : Kernel α γ) (a : α) (x : γ) : ℝ :=
if hα : Countable α then ((κ a).rnDeriv (η a) x).toReal
else
haveI := hαγ.countableOrCountablyGenerated.resolve_left hα
density (map κ (fun a ↦ (a, ()))) η a x univ
