English
Let κ and η be finite kernels. The equality withDensity η (rnDeriv κ η) a = 0 is equivalent to the measure κ a being zero on the complement of the mutually singular set slice at a.
Русский
Пусть κ и η — конечные ядра. Равенство withDensity η (rnDeriv κ η) a = 0 эквивалентно тому, что мера κ a равна нулю на дополнении к сечению взаимной сингулярности при a.
LaTeX
$$$withDensity\\ η\\ (rnDeriv\\ κ\\ η)\\ a = 0 \\iff κ\\ a\\bigl((mutuallySingularSetSlice\\ κ\\ η\\ a)^{c}\\bigr) = 0$$$
Lean4
theorem withDensity_rnDeriv_eq_zero_iff_measure_eq_zero (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
(a : α) : withDensity η (rnDeriv κ η) a = 0 ↔ κ a (mutuallySingularSetSlice κ η a)ᶜ = 0 :=
by
have h_eq_add := rnDeriv_add_singularPart κ η
simp_rw [Kernel.ext_iff, Measure.ext_iff] at h_eq_add
specialize h_eq_add a (mutuallySingularSetSlice κ η a)ᶜ (measurableSet_mutuallySingularSetSlice κ η a).compl
simp only [coe_add, Pi.add_apply, Measure.coe_add, singularPart_compl_mutuallySingularSetSlice κ η,
add_zero] at h_eq_add
rw [← h_eq_add]
exact withDensity_rnDeriv_eq_zero_iff_apply_eq_zero κ η a
