Documentation

Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

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.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