Theorems · Theorem · measure theory

MeasureTheory.Measure.rnDeriv_lt_top

∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤

The Radon-Nikodym derivative of a sigma-finite measure μ with respect to another measure ν is ν-almost everywhere finite.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Cited by

21 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite