# 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.

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
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.iterate {α : Type u_1} {μa : measure_theory.measure α} {f : α → α} (hf : μa) (n : ) :
theorem measure_theory.measure_preserving.skew_product {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {μd : measure_theory.measure δ} {f : α → β} (hf : μb) {g : α → γ → δ} (hgm : measurable ) (hg : ∀ᵐ (x : α) ∂μa, (measure_theory.measure.map (g x)) μc = μd) :
measure_theory.measure_preserving (λ (p : α × γ), (f p.fst, g p.fst p.snd)) (μa.prod μc) (μb.prod μd)
theorem measure_theory.measure_preserving.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {μd : measure_theory.measure δ} {f : α → β} {g : γ → δ} (hf : μb) (hg : μd) :
(μa.prod μc) (μb.prod μd)

If f : α → β sends the measure μa to μb and g : γ → δ sends the measure μc to μd, then prod.map f g sends μa.prod μc to μb.prod μd.

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.