English
If r ≠ 0, the singular part is invariant under multiplying ν by r: μ.singularPart (r ν) = μ.singularPart ν.
Русский
Если r ≠ 0, сингулярная часть сохраняется при умножении ν на r: μ.singularPart (r ν) = μ.singularPart ν.
LaTeX
$$$ r\\neq 0 \\Rightarrow μ.singularPart (r·ν) = μ.singularPart ν $$$
Lean4
/-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
measurable function such that `μ = s + fν`, then `f = μ.rnDeriv ν`.
This theorem provides the uniqueness of the `rnDeriv` in the Lebesgue decomposition
theorem, while `MeasureTheory.Measure.eq_singularPart` provides the uniqueness of the
`singularPart`. Here, the uniqueness is given in terms of the functions, while the uniqueness in
terms of the functions is given in `eq_withDensity_rnDeriv`. -/
theorem eq_rnDeriv [SigmaFinite ν] {s : Measure α} {f : α → ℝ≥0∞} (hf : Measurable f) (hs : s ⟂ₘ ν)
(hadd : μ = s + ν.withDensity f) : f =ᵐ[ν] μ.rnDeriv ν :=
eq_rnDeriv₀ hf.aemeasurable hs hadd
