Theorems · Theorem · measure theory

MeasureTheory.Measure.rnDeriv_div_rnDeriv_eq_div_rnDeriv_add

∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ξ],
  μ.AbsolutelyContinuous ξ →
    ν.AbsolutelyContinuous ξ →
      (fun x => μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x => μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFiniteMeasureTheory.SigmaFiniteMeasureTheory.SigmaFinite