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
MeasureTheory.MeasurePreserving 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
MeasureTheory.MeasurePreserving
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μa : autoParam (MeasureTheory.Measure α) _auto✝)
(μb : autoParam (MeasureTheory.Measure β) _auto✝)
:
f is a measure preserving map w.r.t. measures μa and μb if f is measurable
and map f μa = μb.
- measurable : Measurable f
- map_eq : MeasureTheory.Measure.map f μa = μb
Instances For
theorem
Measurable.measurePreserving
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
(h : Measurable f)
(μa : MeasureTheory.Measure α)
:
theorem
MeasureTheory.MeasurePreserving.id
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
:
theorem
MeasureTheory.MeasurePreserving.aemeasurable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
:
theorem
MeasureTheory.MeasurePreserving.of_isEmpty
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[IsEmpty β]
(f : α → β)
(μa : MeasureTheory.Measure α)
(μb : MeasureTheory.Measure β)
:
theorem
MeasureTheory.MeasurePreserving.symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
(h : MeasureTheory.MeasurePreserving ⇑e)
:
MeasureTheory.MeasurePreserving ⇑e.symm
theorem
MeasureTheory.MeasurePreserving.restrict_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.MeasurePreserving.restrict_preimage_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
(h₂ : MeasurableEmbedding f)
(s : Set β)
:
theorem
MeasureTheory.MeasurePreserving.restrict_image_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
(h₂ : MeasurableEmbedding f)
(s : Set α)
:
theorem
MeasureTheory.MeasurePreserving.aemeasurable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
(h₂ : MeasurableEmbedding f)
{g : β → γ}
:
AEMeasurable (g ∘ f) ↔ AEMeasurable g
theorem
MeasureTheory.MeasurePreserving.quasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
:
theorem
MeasureTheory.MeasurePreserving.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ}
{g : β → γ}
{f : α → β}
(hg : MeasureTheory.MeasurePreserving g)
(hf : MeasureTheory.MeasurePreserving f)
:
theorem
MeasureTheory.MeasurePreserving.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{e : α ≃ᵐ β}
{e' : β ≃ᵐ γ}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ}
(h : MeasureTheory.MeasurePreserving ⇑e)
(h' : MeasureTheory.MeasurePreserving ⇑e')
:
MeasureTheory.MeasurePreserving ⇑(e.trans e')
An alias of MeasureTheory.MeasurePreserving.comp with a convenient defeq and argument order
for MeasurableEquiv
theorem
MeasureTheory.MeasurePreserving.comp_left_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ}
{g : α → β}
{e : β ≃ᵐ γ}
(h : MeasureTheory.MeasurePreserving ⇑e)
:
theorem
MeasureTheory.MeasurePreserving.comp_right_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ}
{g : α → β}
{e : γ ≃ᵐ α}
(h : MeasureTheory.MeasurePreserving ⇑e)
:
theorem
MeasureTheory.MeasurePreserving.sigmaFinite
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
[MeasureTheory.SigmaFinite μb]
:
theorem
MeasureTheory.MeasurePreserving.measure_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.MeasurePreserving.measure_preimage_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f)
(hfe : MeasurableEmbedding f)
(s : Set β)
:
theorem
MeasureTheory.MeasurePreserving.iterate
{α : Type u_1}
[MeasurableSpace α]
{μa : MeasureTheory.Measure α}
{f : α → α}
(hf : MeasureTheory.MeasurePreserving f)
(n : ℕ)
:
theorem
MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → α}
{s : Set α}
(hf : MeasureTheory.MeasurePreserving f)
(hs : MeasurableSet s)
(n : ℕ)
:
theorem
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → α}
{s : Set α}
(hf : MeasureTheory.MeasurePreserving f)
(hs : MeasurableSet 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
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f : α → α}
{s : Set α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : MeasureTheory.MeasurePreserving f)
(hs : MeasurableSet 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 MeasureTheory.MeasurePreserving.conservative and theorems about
MeasureTheory.Conservative.
theorem
MeasureTheory.MeasurableEquiv.measurePreserving_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(e : α ≃ᵐ β)
:
MeasureTheory.MeasurePreserving ⇑e.symm