Radon-Nikodym derivatives of vector measures

This file contains results about Radon-Nikodym derivatives of signed measures that depend both on the Lebesgue decomposition of signed measures and the theory of Radon-Nikodym derivatives of usual measures.

theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [SigmaFinite μ] (h : VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure) : μ.withDensityᵥ (s.rnDeriv μ) = s

theorem MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (μ : Measure α) [SigmaFinite μ] : VectorMeasure.AbsolutelyContinuous s μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s

The Radon-Nikodym theorem for signed measures.

theorem MeasureTheory.withDensityᵥ_rnDeriv_smul {α : Type u_1} {m : MeasurableSpace α} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ ν : Measure α} [μ.HaveLebesgueDecomposition ν] [SigmaFinite μ] {f : α → E} (hμν : μ.AbsolutelyContinuous ν) (hf : Integrable f μ) : (ν.withDensityᵥ fun (x : α) => (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f