Theorems · Theorem · measure theory

MeasureTheory.MeasurePreserving.singularPart

∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.SigmaFinite ν] {f : X → X},
  MeasureTheory.MeasurePreserving f μ μ →
    MeasureTheory.MeasurePreserving f ν ν → MeasureTheory.MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν)

The singular part of a finite invariant measure of a self-map with respect to a σ-finite invariant measure is an invariant measure.

Defined in

Mathlib.Dynamics.Ergodic.RadonNikodym

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.SigmaFinite