Theorems · Theorem · measure theory

MeasureTheory.MeasurePreserving.rnDeriv_comp_aeEq

∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : X → X},
  MeasureTheory.MeasurePreserving f μ μ → MeasureTheory.MeasurePreserving f ν ν → μ.rnDeriv ν ∘ f =ᵐ[ν] μ.rnDeriv ν

The Radon-Nikodym derivative of a finite invariant measure of a self-map f with respect to another finite invariant measure of f is a.e. invariant under f.

Defined in

Mathlib.Dynamics.Ergodic.RadonNikodym

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure