# mathlibdocumentation

dynamics.ergodic.measure_preserving

# 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 measure_theory.measure_preserving 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 measure_theory.measure_preserving {α : Type u_1} {β : Type u_2} (f : α → β) (μa : . "volume_tac") (μb : . "volume_tac") :
Prop
• measurable :
• map_eq : = μb

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

@[protected]
theorem measurable.measure_preserving {α : Type u_1} {β : Type u_2} {f : α → β} (h : measurable f) (μa : measure_theory.measure α) :
@[protected]
theorem measure_theory.measure_preserving.id {α : Type u_1} (μ : measure_theory.measure α) :
@[protected]
theorem measure_theory.measure_preserving.ae_measurable {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) :
μa
theorem measure_theory.measure_preserving.symm {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) {μa : measure_theory.measure α} {μb : measure_theory.measure β} (h : μb) :
μa
theorem measure_theory.measure_preserving.restrict_preimage {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) {s : set β} (hs : measurable_set s) :
(μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem measure_theory.measure_preserving.restrict_preimage_emb {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) (h₂ : measurable_embedding f) (s : set β) :
(μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem measure_theory.measure_preserving.restrict_image_emb {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) (h₂ : measurable_embedding f) (s : set α) :
(μb.restrict (f '' s))
theorem measure_theory.measure_preserving.ae_measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) (h₂ : measurable_embedding f) {g : β → γ} :
ae_measurable (g f) μa μb
@[protected]
theorem measure_theory.measure_preserving.quasi_measure_preserving {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) :
theorem measure_theory.measure_preserving.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {g : β → γ} {f : α → β} (hg : μc) (hf : μb) :
μa μc
@[protected]
theorem measure_theory.measure_preserving.sigma_finite {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb)  :
theorem measure_theory.measure_preserving.measure_preimage {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) {s : set β} (hs : measurable_set s) :
μa (f ⁻¹' s) = μb s
theorem measure_theory.measure_preserving.measure_preimage_emb {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : μb) (hfe : measurable_embedding f) (s : set β) :
μa (f ⁻¹' s) = μb s
@[protected]
theorem measure_theory.measure_preserving.iterate {α : Type u_1} {μa : measure_theory.measure α} {f : α → α} (hf : μa) (n : ) :
theorem measure_theory.measure_preserving.exists_mem_image_mem_of_volume_lt_mul_volume {α : Type u_1} {μ : measure_theory.measure α} {f : α → α} {s : set α} (hf : μ) (hs : measurable_set s) {n : } (hvol : < n * μ s) :
∃ (x : α) (H : x s) (m : ) (H : m 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 measure_theory.measure_preserving.exists_mem_image_mem {α : Type u_1} {μ : measure_theory.measure α} {f : α → α} {s : set α} (hf : μ) (hs : measurable_set s) (hs' : μ s 0) :
∃ (x : α) (H : x s) (m : ) (H : 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 measure_theory.measure_preserving.conservative and theorems about measure_theory.conservative.