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 : Measure α := by volume_tac)
(μb : Measure β := by volume_tac)
:
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 : 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 α]
(μ : Measure α)
:
MeasurePreserving id μ μ
theorem
MeasureTheory.MeasurePreserving.aemeasurable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
:
AEMeasurable f μa
theorem
MeasureTheory.MeasurePreserving.of_isEmpty
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[IsEmpty β]
(f : α → β)
(μa : Measure α)
(μb : Measure β)
:
MeasurePreserving f μa μb
theorem
MeasureTheory.MeasurePreserving.symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
{μa : Measure α}
{μb : Measure β}
(h : MeasurePreserving (⇑e) μa μb)
:
MeasurePreserving (⇑e.symm) μb μa
theorem
MeasureTheory.MeasurePreserving.restrict_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
{s : Set β}
(hs : MeasurableSet s)
:
MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem
MeasureTheory.MeasurePreserving.restrict_preimage_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
(h₂ : MeasurableEmbedding f)
(s : Set β)
:
MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
theorem
MeasureTheory.MeasurePreserving.restrict_image_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
(h₂ : MeasurableEmbedding f)
(s : Set α)
:
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 : Measure α}
{μb : Measure β}
{f : α → β}
(hf : 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 : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
:
Measure.QuasiMeasurePreserving f μa μb
theorem
MeasureTheory.MeasurePreserving.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : Measure α}
{μb : Measure β}
{μc : Measure γ}
{g : β → γ}
{f : α → β}
(hg : MeasurePreserving g μb μc)
(hf : MeasurePreserving f μa μb)
:
MeasurePreserving (g ∘ f) μa μc
theorem
MeasureTheory.MeasurePreserving.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{e : α ≃ᵐ β}
{e' : β ≃ᵐ γ}
{μa : Measure α}
{μb : Measure β}
{μc : Measure γ}
(h : MeasurePreserving (⇑e) μa μb)
(h' : MeasurePreserving (⇑e') μb μc)
:
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 : Measure α}
{μb : Measure β}
{μc : Measure γ}
{g : α → β}
{e : β ≃ᵐ γ}
(h : MeasurePreserving (⇑e) μb μc)
:
MeasurePreserving (⇑e ∘ g) μa μc ↔ MeasurePreserving g μa μb
theorem
MeasureTheory.MeasurePreserving.comp_right_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : Measure α}
{μb : Measure β}
{μc : Measure γ}
{g : α → β}
{e : γ ≃ᵐ α}
(h : MeasurePreserving (⇑e) μc μa)
:
MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasurePreserving g μa μb
theorem
MeasureTheory.MeasurePreserving.sigmaFinite
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
[SigmaFinite μb]
:
SigmaFinite μa
theorem
MeasureTheory.MeasurePreserving.measure_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
{s : Set β}
(hs : NullMeasurableSet s μb)
:
theorem
MeasureTheory.MeasurePreserving.measure_preimage_emb
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
(hfe : MeasurableEmbedding f)
(s : Set β)
:
theorem
MeasureTheory.MeasurePreserving.measure_preimage_equiv
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α ≃ᵐ β}
(hf : MeasurePreserving (⇑f) μa μb)
(s : Set β)
:
theorem
MeasureTheory.MeasurePreserving.aeconst_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μa : Measure α}
{μb : Measure β}
[MeasurableSingletonClass γ]
{f : α → β}
(hf : MeasurePreserving f μa μb)
{g : β → γ}
(hg : NullMeasurable g μb)
:
Filter.EventuallyConst (g ∘ f) (ae μa) ↔ Filter.EventuallyConst g (ae μb)
theorem
MeasureTheory.MeasurePreserving.aeconst_preimage
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : MeasurePreserving f μa μb)
{s : Set β}
(hs : NullMeasurableSet s μb)
:
Filter.EventuallyConst (f ⁻¹' s) (ae μa) ↔ Filter.EventuallyConst s (ae μb)
theorem
MeasureTheory.MeasurePreserving.add_measure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{f : α → β}
{μa' : Measure α}
{μb' : Measure β}
(hf : MeasurePreserving f μa μb)
(hf' : MeasurePreserving f μa' μb')
:
MeasurePreserving f (μa + μa') (μb + μb')
theorem
MeasureTheory.MeasurePreserving.smul_measure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μa : Measure α}
{μb : Measure β}
{R : Type u_5}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{f : α → β}
(hf : MeasurePreserving f μa μb)
(c : R)
:
MeasurePreserving f (c • μa) (c • μb)
theorem
MeasureTheory.MeasurePreserving.iterate
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → α}
(hf : MeasurePreserving f μ μ)
(n : ℕ)
:
MeasurePreserving f^[n] μ μ
theorem
MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → α}
{s : Set α}
(hf : MeasurePreserving f μ μ)
(hs : NullMeasurableSet s μ)
(n : ℕ)
:
theorem
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → α}
{s : Set α}
(hf : MeasurePreserving f μ μ)
(hs : NullMeasurableSet 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.
@[deprecated MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure (since := "2024-08-12")]
theorem
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → α}
{s : Set α}
(hf : MeasurePreserving f μ μ)
(hs : NullMeasurableSet s μ)
{n : ℕ}
(hvol : μ Set.univ < ↑n * μ s)
:
Alias of MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure.
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 α]
{μ : Measure α}
{f : α → α}
{s : Set α}
[IsFiniteMeasure μ]
(hf : MeasurePreserving f μ μ)
(hs : NullMeasurableSet 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 β]
(μ : Measure α)
(e : α ≃ᵐ β)
:
MeasurePreserving (⇑e.symm) (Measure.map (⇑e) μ) μ