English
The signed measure rnDeriv s μ is defined as the difference of the RN derivatives of the positive and negative Jordan parts of s with respect to μ.
Русский
Знакованная мера rnDeriv s μ задаётся как разность rnDeriv положительной и отрицательной частей Джорданова разложения s по μ.
LaTeX
$$rnDeriv (s) μ = (s.toJordanDecomposition.posPart.rnDeriv μ) - (s.toJordanDecomposition.negPart.rnDeriv μ)$$
Lean4
/-- The Radon-Nikodym derivative between a signed measure and a positive measure.
`rnDeriv s μ` satisfies `μ.withDensityᵥ (s.rnDeriv μ) = s`
if and only if `s` is absolutely continuous with respect to `μ` and this fact is known as
`MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensity_rnDeriv_eq`
and can be found in `Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean`. -/
def rnDeriv (s : SignedMeasure α) (μ : Measure α) : α → ℝ := fun x =>
(s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
