# 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

source
structure MeasureTheory.MeasurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μa : Measure α := by volume_tac) (μb : Measure β := by 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`.

- measurable : Measurable f
- map_eq : Measure.map f μa = μb

Instances For

source
theorem Measurable.measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (h : Measurable f) (μa : MeasureTheory.Measure α) :
MeasureTheory.MeasurePreserving f μa (MeasureTheory.Measure.map f μa)
source
theorem MeasureTheory.MeasurePreserving.id {α : Type u_1} [MeasurableSpace α] (μ : Measure α) :
MeasurePreserving id μ μ
source
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
source
theorem MeasureTheory.MeasurePreserving.of_isEmpty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty β] (f : α → β) (μa : Measure α) (μb : Measure β) :
MeasurePreserving f μa μb
source
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
source
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)
source
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)
source
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))
source
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
source
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
source
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
source
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`

source
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
source
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
source
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
source
theorem MeasureTheory.MeasurePreserving.sfinite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : Measure α} {μb : Measure β} {f : α → β} (hf : MeasurePreserving f μa μb) [SFinite μa] :
SFinite μb
source
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) :
μa (f ⁻¹' s) = μb s
source
theorem MeasureTheory.MeasurePreserving.measureReal_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) :
μa.real (f ⁻¹' s) = μb.real s
source
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 β) :
μa (f ⁻¹' s) = μb s
source
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 β) :
μa (⇑f ⁻¹' s) = μb s
source
theorem MeasureTheory.MeasurePreserving.measure_preimage_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : Measure α} {μb : Measure β} {f : α → β} (hf : MeasurePreserving f μa μb) (s : Set β) :
μa (f ⁻¹' s) ≤ μb s
source
theorem MeasureTheory.MeasurePreserving.preimage_null {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : Measure α} {μb : Measure β} {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β} (hs : μb s = 0) :
μa (f ⁻¹' s) = 0
source
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)
source
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)
source
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')
source
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)
source
theorem MeasureTheory.MeasurePreserving.iterate {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → α} (hf : MeasurePreserving f μ μ) (n : ℕ) :
MeasurePreserving f^[n] μ μ
source
theorem MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → α} {s : Set α} (hf : MeasurePreserving f μ μ) (hs : NullMeasurableSet s μ) (n : ℕ) :
μ (symmDiff s (f^[n] ⁻¹' s)) ≤ n • μ (symmDiff s (f ⁻¹' s))
source
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) :
∃ x ∈ s, ∃ 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`.

source
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) :
∃ x ∈ s, ∃ (m : ℕ), 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 `MeasureTheory.MeasurePreserving.conservative` and theorems about `MeasureTheory.Conservative`.

source
theorem MeasureTheory.measurePreserving_subtype_coe {α : Type u_1} [MeasurableSpace α] {μa : Measure α} {s : Set α} (hs : MeasurableSet s) :
MeasurePreserving Subtype.val (Measure.comap Subtype.val μa) (μa.restrict s)
source
theorem MeasureTheory.MeasurableEquiv.measurePreserving_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) (e : α ≃ᵐ β) :
MeasurePreserving (⇑e.symm) (Measure.map (⇑e) μ) μ