mathlib documentation

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} [measurable_space α] [measurable_space β] (f : α → β) (μa : measure_theory.measure α . "volume_tac") (μb : measure_theory.measure β . "volume_tac") :
Prop

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} [measurable_space α] [measurable_space β] {f : α → β} (h : measurable f) (μa : measure_theory.measure α) :
@[protected]
theorem measure_theory.measure_preserving.ae_measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : measure_theory.measure_preserving f μa μb) :
theorem measure_theory.measure_preserving.restrict_preimage {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : measure_theory.measure_preserving f μa μb) {s : set β} (hs : measurable_set s) :
theorem measure_theory.measure_preserving.restrict_image_emb {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : measure_theory.measure_preserving f μa μb) (h₂ : measurable_embedding f) (s : set α) :
theorem measure_theory.measure_preserving.ae_measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : measure_theory.measure_preserving f μa μb) (h₂ : measurable_embedding f) {g : β → γ} :
theorem measure_theory.measure_preserving.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {g : β → γ} {f : α → β} (hg : measure_theory.measure_preserving g μb μc) (hf : measure_theory.measure_preserving f μa μb) :
theorem measure_theory.measure_preserving.measure_preimage {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : measure_theory.measure_preserving f μa μ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} [measurable_space α] [measurable_space β] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (hf : measure_theory.measure_preserving f μa μb) (hfe : measurable_embedding f) (s : set β) :
μa (f ⁻¹' s) = μb s
@[protected]
theorem measure_theory.measure_preserving.exists_mem_image_mem_of_volume_lt_mul_volume {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → α} {s : set α} (hf : measure_theory.measure_preserving f μ μ) (hs : measurable_set s) {n : } (hvol : μ set.univ < n * μ s) :
∃ (x : α) (H : x s) (m : ) (H : m set.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 measure_theory.measure_preserving.exists_mem_image_mem {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → α} {s : set α} [measure_theory.is_finite_measure μ] (hf : measure_theory.measure_preserving f μ μ) (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.