English
For kernels κ and η, the singular part κ a with respect to η a evaluated as a function over a equals the pointwise singularPart of the measures κ a and η a.
Русский
Для ядер κ и η сингулярная часть κ a относительно η a является функцией от a и равна точечной сингулярной части мер κ a и η a.
LaTeX
$$$\\text{singularPart }κ η a = (κ a).\\text{singularPart}(η a)$$$
Lean4
theorem singularPart_eq_zero_iff_measure_eq_zero (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
singularPart κ η 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)
simp only [coe_add, Pi.add_apply, Measure.coe_add, withDensity_rnDeriv_mutuallySingularSetSlice κ η,
zero_add] at h_eq_add
rw [← h_eq_add]
exact singularPart_eq_zero_iff_apply_eq_zero κ η a
