Documentation

Mathlib.Dynamics.Ergodic.MeasurePreserving

Measure preserving maps #

We say that f : α → β is a measure preserving map w.r.t. measures μ : Measure α and ν : Measure β if f is measurable and map f μ = ν. In this file we define the predicate MeasureTheory.MeasurePreserving and prove its basic properties.

We use the term "measure preserving" because in many applications α = β and μ = ν.

References #

Partially based on this Isabelle formalization.

Tags #

measure preserving map, measure

f is a measure preserving map w.r.t. measures μa and μb if f is measurable and map f μa = μb.

Instances For
    theorem MeasureTheory.MeasurePreserving.restrict_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) {s : Set β} (hs : MeasurableSet s) :
    MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
    theorem MeasureTheory.MeasurePreserving.restrict_preimage_emb {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) (s : Set β) :
    MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
    theorem MeasureTheory.MeasurePreserving.restrict_image_emb {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) (s : Set α) :
    MeasureTheory.MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))
    theorem MeasureTheory.MeasurePreserving.aemeasurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) {g : βγ} :
    theorem MeasureTheory.MeasurePreserving.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {g : βγ} {f : αβ} (hg : MeasureTheory.MeasurePreserving g μb μc) (hf : MeasureTheory.MeasurePreserving f μa μb) :
    theorem MeasureTheory.MeasurePreserving.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {e : α ≃ᵐ β} {e' : β ≃ᵐ γ} {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} (h : MeasureTheory.MeasurePreserving (⇑e) μa μb) (h' : MeasureTheory.MeasurePreserving (⇑e') μb μc) :
    MeasureTheory.MeasurePreserving (⇑(e.trans e')) μa μc

    An alias of MeasureTheory.MeasurePreserving.comp with a convenient defeq and argument order for MeasurableEquiv

    theorem MeasureTheory.MeasurePreserving.measure_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) {s : Set β} (hs : MeasureTheory.NullMeasurableSet s μb) :
    μa (f ⁻¹' s) = μb s
    theorem MeasureTheory.MeasurePreserving.measure_preimage_emb {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) (hfe : MeasurableEmbedding f) (s : Set β) :
    μa (f ⁻¹' s) = μb s
    theorem MeasureTheory.MeasurePreserving.measure_preimage_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α ≃ᵐ β} (hf : MeasureTheory.MeasurePreserving (⇑f) μa μb) (s : Set β) :
    μa (f ⁻¹' s) = μb s
    theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : αα} {s : Set α} (hf : MeasureTheory.MeasurePreserving f μ μ) (hs : MeasureTheory.NullMeasurableSet s μ) {n : } (hvol : μ Set.univ < n * μ s) :
    xs, mSet.Ioo 0 n, f^[m] x s

    If μ univ < n * μ s and f is a map preserving measure μ, then for some x ∈ s and 0 < m < n, f^[m] x ∈ s.

    @[deprecated MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure]
    theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : αα} {s : Set α} (hf : MeasureTheory.MeasurePreserving f μ μ) (hs : MeasureTheory.NullMeasurableSet s μ) {n : } (hvol : μ Set.univ < n * μ s) :
    xs, mSet.Ioo 0 n, f^[m] x s

    Alias of MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure.


    If μ univ < n * μ s and f is a map preserving measure μ, then for some x ∈ s and 0 < m < n, f^[m] x ∈ s.

    theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : αα} {s : Set α} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.MeasurePreserving f μ μ) (hs : MeasureTheory.NullMeasurableSet s μ) (hs' : μ s 0) :
    xs, ∃ (m : ), m 0 f^[m] x s

    A self-map preserving a finite measure is conservative: if μ s ≠ 0, then at least one point x ∈ s comes back to s under iterations of f. Actually, a.e. point of s comes back to s infinitely many times, see MeasureTheory.MeasurePreserving.conservative and theorems about MeasureTheory.Conservative.