English
For kernels κ and η, κ a and η a are mutually singular for a fixed a if and only if the singular part of κ a with respect to η a equals κ a minus its absolutely continuous part with respect to η a.
Русский
Для ядер κ и η множества κ a и η a взаимно сингулярны по a тогда и только тогда, когда сингулярная часть κ a по отношению к η a равна κ a минус абсолютно непрерывная часть по η a.
LaTeX
$$$(κ a) \\perp\\!\\!\\!_{m} (η a) \\iff (κ a) = (κ a)_{\\text{ac}} + (κ a)_{\\text{sing}}$ и $ (κ a)_{\\text{sing}} = κ a - (κ a)_{\\text{ac}}$$$
Lean4
theorem withDensity_rnDeriv_eq_zero_iff_mutuallySingular (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
(a : α) : withDensity η (rnDeriv κ η) a = 0 ↔ κ a ⟂ₘ η a :=
by
conv_rhs => rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [h, zero_add]
exact mutuallySingular_singularPart _ _ _
rw [Measure.MutuallySingular.add_left_iff] at h
rw [← Measure.MutuallySingular.self_iff]
exact h.1.mono_ac Measure.AbsolutelyContinuous.rfl (withDensity_absolutelyContinuous (κ := η) (rnDeriv κ η) a)
