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.

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.skew_product {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {μd : measure_theory.measure δ} [measure_theory.sigma_finite μb] [measure_theory.sigma_finite μd] {f : α → β} (hf : measure_theory.measure_preserving f μa μb) {g : α → γ → δ} (hgm : measurable (function.uncurry g)) (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} [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {μd : measure_theory.measure δ} [measure_theory.sigma_finite μb] [measure_theory.sigma_finite μd] {f : α → β} {g : γ → δ} (hf : measure_theory.measure_preserving f μa μb) (hg : measure_theory.measure_preserving g μc μ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} [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.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.