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
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
- 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
.
If μ univ < n * μ s
and f
is a map preserving measure μ
,
then for some x ∈ s
and 0 < m < n
, 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 measure_theory.measure_preserving.conservative
and theorems about
measure_theory.conservative
.