# 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

structure MeasureTheory.MeasurePreserving {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (μa : ) (μb : ) :

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

• measurable :
• map_eq : = μb
Instances For
theorem MeasureTheory.MeasurePreserving.measurable {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {μa : } {μb : } (self : ) :
theorem MeasureTheory.MeasurePreserving.map_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {μa : } {μb : } (self : ) :
= μb
theorem Measurable.measurePreserving {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (h : ) (μa : ) :
theorem MeasureTheory.MeasurePreserving.id {α : Type u_1} [] (μ : ) :
theorem MeasureTheory.MeasurePreserving.aemeasurable {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) :
theorem MeasureTheory.MeasurePreserving.of_isEmpty {α : Type u_1} {β : Type u_2} [] [] [] (f : αβ) (μa : ) (μb : ) :
theorem MeasureTheory.MeasurePreserving.symm {α : Type u_1} {β : Type u_2} [] [] (e : α ≃ᵐ β) {μa : } {μb : } (h : MeasureTheory.MeasurePreserving (e) μa μb) :
theorem MeasureTheory.MeasurePreserving.restrict_preimage {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) {s : Set β} (hs : ) :
MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem MeasureTheory.MeasurePreserving.restrict_preimage_emb {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) (h₂ : ) (s : Set β) :
MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem MeasureTheory.MeasurePreserving.restrict_image_emb {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) (h₂ : ) (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} [] [] [] {μa : } {μb : } {f : αβ} (hf : ) (h₂ : ) {g : βγ} :
theorem MeasureTheory.MeasurePreserving.quasiMeasurePreserving {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) :
theorem MeasureTheory.MeasurePreserving.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {μa : } {μb : } {μc : } {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem MeasureTheory.MeasurePreserving.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e : α ≃ᵐ β} {e' : β ≃ᵐ γ} {μa : } {μb : } {μc : } (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.comp_left_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {μa : } {μb : } {μc : } {g : αβ} {e : β ≃ᵐ γ} (h : MeasureTheory.MeasurePreserving (e) μb μc) :
theorem MeasureTheory.MeasurePreserving.comp_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {μa : } {μb : } {μc : } {g : αβ} {e : γ ≃ᵐ α} (h : MeasureTheory.MeasurePreserving (e) μc μa) :
theorem MeasureTheory.MeasurePreserving.sigmaFinite {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) :
theorem MeasureTheory.MeasurePreserving.measure_preimage {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) {s : Set β} (hs : ) :
μa (f ⁻¹' s) = μb s
theorem MeasureTheory.MeasurePreserving.measure_preimage_emb {α : Type u_1} {β : Type u_2} [] [] {μa : } {μb : } {f : αβ} (hf : ) (hfe : ) (s : Set β) :
μa (f ⁻¹' s) = μb s
theorem MeasureTheory.MeasurePreserving.iterate {α : Type u_1} [] {μa : } {f : αα} (hf : ) (n : ) :
theorem MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le {α : Type u_1} [] {μ : } {f : αα} {s : Set α} (hf : ) (hs : ) (n : ) :
μ (symmDiff s (f^[n] ⁻¹' s)) n μ (symmDiff s (f ⁻¹' s))
theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume {α : Type u_1} [] {μ : } {f : αα} {s : Set α} (hf : ) (hs : ) {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.

theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem {α : Type u_1} [] {μ : } {f : αα} {s : Set α} (hf : ) (hs : ) (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.

theorem MeasureTheory.MeasurableEquiv.measurePreserving_symm {α : Type u_1} {β : Type u_2} [] [] (μ : ) (e : α ≃ᵐ β) :