Measure preserving maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
- measurable : measurable f
- map_eq : measure_theory.measure.map 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.
@[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.id
{α : Type u_1}
[measurable_space α]
(μ : 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) :
ae_measurable f μa
theorem
measure_theory.measure_preserving.symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(e : α ≃ᵐ β)
{μa : measure_theory.measure α}
{μb : measure_theory.measure β}
(h : measure_theory.measure_preserving ⇑e μa μb) :
measure_theory.measure_preserving ⇑(e.symm) μb μa
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) :
measure_theory.measure_preserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem
measure_theory.measure_preserving.restrict_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)
(h₂ : measurable_embedding f)
(s : set β) :
measure_theory.measure_preserving f (μa.restrict (f ⁻¹' s)) (μb.restrict 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 α) :
measure_theory.measure_preserving f (μa.restrict s) (μb.restrict (f '' s))
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 : β → γ} :
ae_measurable (g ∘ f) μa ↔ ae_measurable g μb
@[protected]
theorem
measure_theory.measure_preserving.quasi_measure_preserving
{α : 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) :
@[protected]
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) :
measure_theory.measure_preserving (g ∘ f) μa μc
@[protected]
theorem
measure_theory.measure_preserving.comp_left_iff
{α : 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 : α → β}
{e : β ≃ᵐ γ}
(h : measure_theory.measure_preserving ⇑e μb μc) :
measure_theory.measure_preserving (⇑e ∘ g) μa μc ↔ measure_theory.measure_preserving g μa μb
@[protected]
theorem
measure_theory.measure_preserving.comp_right_iff
{α : 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 : α → β}
{e : γ ≃ᵐ α}
(h : measure_theory.measure_preserving ⇑e μc μa) :
measure_theory.measure_preserving (g ∘ ⇑e) μc μb ↔ measure_theory.measure_preserving g μa μb
@[protected]
theorem
measure_theory.measure_preserving.sigma_finite
{α : 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)
[measure_theory.sigma_finite μ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) :
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 β) :
@[protected]
theorem
measure_theory.measure_preserving.iterate
{α : Type u_1}
[measurable_space α]
{μa : measure_theory.measure α}
{f : α → α}
(hf : measure_theory.measure_preserving f μa μa)
(n : ℕ) :
measure_theory.measure_preserving f^[n] μa μa
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) :
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) :
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.
theorem
measure_theory.measurable_equiv.measure_preserving_symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(μ : measure_theory.measure α)
(e : α ≃ᵐ β) :