English
Let κ and η be finite kernels. For every a, the equation withDensity η (rnDeriv κ η) a = 0 holds iff its value on the complement of the mutually singular set slice at a is zero; i.e., the density vanishes exactly outside the mutually singular set slice.
Русский
Пусть κ и η — конечные ядра. Для каждого a выполняется равенство сDensity η (rnDeriv κ η) a = 0 тогда и только тогда, когда его значение на дополнении от сечения взаимной сингулярности на a равно нулю; то есть плотность нулевая ровно за пределами сечения взаимной сингулярности.
LaTeX
$$$withDensity\\ η\\ (rnDeriv\\ κ\\ η)\\ a = 0 \\iff withDensity\\ η\\ (rnDeriv\\ κ\\ η)\\ a\\bigl(mutuallySingularSetSlice\\ κ\\ η\\ a\bigr)^{c} = 0$$$
Lean4
theorem withDensity_rnDeriv_eq_zero_iff_apply_eq_zero (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
withDensity η (rnDeriv κ η) a = 0 ↔ withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a)ᶜ = 0 :=
by
rw [← Measure.measure_univ_eq_zero]
have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp
rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]
