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
MeasureTheory.MeasurePreserving.measurable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{μa : autoParam (MeasureTheory.Measure α) _auto✝}
{μb : autoParam (MeasureTheory.Measure β) _auto✝}
(self : MeasureTheory.MeasurePreserving f μa μb)
:
theorem
MeasureTheory.MeasurePreserving.map_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → β}
{μa : autoParam (MeasureTheory.Measure α) _auto✝}
{μb : autoParam (MeasureTheory.Measure β) _auto✝}
(self : MeasureTheory.MeasurePreserving f μa μb)
:
MeasureTheory.Measure.map f μa = μb
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 μa μb)
:
AEMeasurable f μa
theorem
MeasureTheory.MeasurePreserving.of_isEmpty
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[IsEmpty β]
(f : α → β)
(μa : MeasureTheory.Measure α)
(μb : MeasureTheory.Measure β)
:
MeasureTheory.MeasurePreserving f μa μb
theorem
MeasureTheory.MeasurePreserving.symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
(h : MeasureTheory.MeasurePreserving (⇑e) μa μb)
:
MeasureTheory.MeasurePreserving (⇑e.symm) μb μa
theorem
MeasureTheory.MeasurePreserving.restrict_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f μa μb)
{s : Set β}
(hs : MeasurableSet s)
:
MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict 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 μa μb)
(h₂ : MeasurableEmbedding f)
(s : Set β)
:
MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
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 μa μb)
(h₂ : MeasurableEmbedding f)
(s : Set α)
:
MeasureTheory.MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))
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 μa μb)
(h₂ : MeasurableEmbedding f)
{g : β → γ}
:
AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb
theorem
MeasureTheory.MeasurePreserving.quasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f μa μb)
:
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 μb μc)
(hf : MeasureTheory.MeasurePreserving f μa μb)
:
MeasureTheory.MeasurePreserving (g ∘ f) μa μc
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) μa μb)
(h' : MeasureTheory.MeasurePreserving (⇑e') μb μc)
:
MeasureTheory.MeasurePreserving (⇑(e.trans e')) μa μc
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) μb μc)
:
MeasureTheory.MeasurePreserving (⇑e ∘ g) μa μc ↔ MeasureTheory.MeasurePreserving g μa μb
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) μc μa)
:
MeasureTheory.MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasureTheory.MeasurePreserving g μa μb
theorem
MeasureTheory.MeasurePreserving.sigmaFinite
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f μa μb)
[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 μa μb)
{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 μa μb)
(hfe : MeasurableEmbedding f)
(s : Set β)
:
theorem
MeasureTheory.MeasurePreserving.iterate
{α : Type u_1}
[MeasurableSpace α]
{μa : MeasureTheory.Measure α}
{f : α → α}
(hf : MeasureTheory.MeasurePreserving f μa μa)
(n : ℕ)
:
MeasureTheory.MeasurePreserving f^[n] μa μa
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) (MeasureTheory.Measure.map (⇑e) μ) μ