Theorems · Theorem · measure theory

MeasureTheory.Measure.rnDeriv_add

∀ {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν₁]
  [MeasureTheory.IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ]
  [(ν₁ + ν₂).HaveLebesgueDecomposition μ], (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Radon-Nikodym derivative of a sum of two measures. See also rnDeriv_add', which requires sigma-finite ν₁, ν₂ and μ.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Cited by

1 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.HaveLebesgueDecompositionMeasureTheory.Measure.HaveLebesgueDecompositionMeasureTheory.Measure.HaveLebesgueDecomposition