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)
:
theorem
MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq
{α : Type u_1}
{m : MeasurableSpace α}
(s : SignedMeasure α)
(μ : Measure α)
[SigmaFinite μ]
:
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 μ)
: