English
The kernel κ is the sum of the absolutely continuous part η.withDensity(κ.rnDeriv η) and its singularPart η.
Русский
Ядро κ есть сумма абсолюто-го непрерывного компонента η.withDensity(κ.rnDeriv η) и его сингулярной части η.
LaTeX
$$$ withDensity(\eta)(rnDeriv(\kappa, \eta)) + singularPart(\kappa, \eta) = \kappa $$$
Lean4
/-- Lebesgue decomposition of a finite kernel `κ` with respect to another one `η`.
`κ` is the sum of an absolutely continuous part `withDensity η (rnDeriv κ η)` and a singular part
`singularPart κ η`. -/
theorem rnDeriv_add_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
withDensity η (rnDeriv κ η) + singularPart κ η = κ :=
by
ext a s hs
rw [← inter_union_diff s (mutuallySingularSetSlice κ η a)]
simp only [coe_add, Pi.add_apply, Measure.coe_add]
have hm := measurableSet_mutuallySingularSetSlice κ η a
simp only [measure_union (Disjoint.mono inter_subset_right le_rfl disjoint_sdiff_right) (hs.diff hm)]
rw [singularPart_of_subset_mutuallySingularSetSlice (hs.inter hm) inter_subset_right,
singularPart_of_subset_compl_mutuallySingularSetSlice (diff_subset_iff.mpr (by simp)), add_zero,
withDensity_rnDeriv_of_subset_mutuallySingularSetSlice inter_subset_right, zero_add,
withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice (hs.diff hm) (diff_subset_iff.mpr (by simp)), add_comm]
