English
Let κ and η be finite kernels on α → γ. For every a in α, the singular part of κ a with respect to η a vanishes exactly when its value on the mutually singular set slice at a vanishes; i.e., the singular part is zero iff it is zero on the slice where κ a and η a are mutually singular.
Русский
Пусть κ и η — конечные ядра на α → γ. Для каждого a ∈ α сингулярная часть κ a по η a исчезает тогда и только тогда, когда её значение на сечении множества mutuallySingularSetSlice κ η a равно нулю; то есть сингулярная часть равна нулю тогда, когда она равна нулю на соответствующей области.
LaTeX
$$$singularPart\\ κ\\ η\\ a = 0 \\iff singularPart\\ κ\\ η\\ a\\bigl(mutuallySingularSetSlice\\ κ\\ η\\ a\bigr) = 0$$$
Lean4
theorem singularPart_eq_zero_iff_apply_eq_zero (κ η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
singularPart κ η a = 0 ↔ singularPart κ η 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,
singularPart_compl_mutuallySingularSetSlice, add_zero]
