Theorems · Theorem · measure theory

MeasureTheory.lintegral_rnDeriv_mul

∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ {f : α → ENNReal}, AEMeasurable f ν → ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.Measure.HaveLebesgueDecomposition