MeasureTheory.MeasurePreserving.measure_preimage
theorem MeasureTheory.MeasurePreserving.measure_preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β},
MeasureTheory.MeasurePreserving f μa μb → ∀ {s : Set β}, MeasurableSet s → ↑↑μa (f ⁻¹' s) = ↑↑μb s
This theorem, `MeasureTheory.MeasurePreserving.measure_preimage`, states that for any two types `α` and `β` with measure spaces, a measure `μa` on `α`, a measure `μb` on `β`, and a function `f` from `α` to `β`, if `f` preserves the measure from `μa` to `μb`, then for any measurable set `s` in `β`, the measure `μa` of the preimage of `s` under `f` is equal to the measure `μb` of `s` itself. In mathematical terms, if `f` is a measure-preserving function from a measurable space `(α, μa)` to another measurable space `(β, μb)`, then for all measurable sets `s` in `β`, the measure of the set of all elements in `α` that get mapped to `s` by `f` (denoted as `f⁻¹' s`) under the measure `μa` is the same as the measure of `s` under the measure `μb`.
More concisely: If `f: α → β` is a measure-preserving function between measurable spaces `(α, μa)` and `(β, μb)`, then for any measurable set `s` in `β`, the measure `μa` of the preimage `f⁻¹' s` is equal to `μb(s)`.
|
MeasureTheory.MeasurePreserving.trans
theorem MeasureTheory.MeasurePreserving.trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {e : α ≃ᵐ β} {e' : β ≃ᵐ γ} {μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ},
MeasureTheory.MeasurePreserving (⇑e) μa μb →
MeasureTheory.MeasurePreserving (⇑e') μb μc → MeasureTheory.MeasurePreserving (⇑(e.trans e')) μa μc
This theorem, `MeasureTheory.MeasurePreserving.trans`, states that given three measurable spaces `α`, `β`, and `γ`, along with measure preserving functions between them encoded as measurable equivalences `e` from `α` to `β` and `e'` from `β` to `γ`. If the measures `μa`, `μb`, and `μc` on the respective spaces are preserved by these functions, then the composition of these functions (denoted by `e.trans e'`), also preserves the measure from `α` to `γ`. In other words, measure preservation is transitive over compositions of measurable equivalences.
More concisely: Given measurable spaces `α`, `β`, `γ` and measurable equivalences `e : α ≃ β` and `e' : β ≃ γ` that preserve measures `μa`, `μb`, and `μc`, respectively, then their composition `e.trans e'` preserves the measure from `α` to `γ`. (Measure preservation is transitive over compositions of measurable equivalences.)
|
MeasureTheory.MeasurePreserving.quasiMeasurePreserving
theorem MeasureTheory.MeasurePreserving.quasiMeasurePreserving :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β},
MeasureTheory.MeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving f μa μb
This theorem states that for all types α and β, given that α and β are measurable spaces, and given measures μa on α and μb on β as well as a function f from α to β, if f is a measure-preserving function from μa to μb, then f is also quasi-measure-preserving. In other words, any function that preserves measures also preserves them in the weaker sense of being quasi-measure-preserving.
More concisely: If $f:\alpha \to \beta$ is a measure-preserving function between measurable spaces $(\alpha, \mu_a)$ and $(\beta, \mu_b)$, then $f$ is quasi-measure-preserving.
|
MeasureTheory.MeasurePreserving.comp
theorem MeasureTheory.MeasurePreserving.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ} {g : β → γ} {f : α → β},
MeasureTheory.MeasurePreserving g μb μc →
MeasureTheory.MeasurePreserving f μa μb → MeasureTheory.MeasurePreserving (g ∘ f) μa μc
This theorem states that if you have three types α, β and γ with respective measurable spaces and corresponding measures μa, μb and μc, and you have two functions, g mapping from β to γ and f mapping from α to β. If it's known that g preserves the measure from μb to μc, and f preserves the measure from μa to μb, then the composition of g and f (g ∘ f) also preserves measure, specifically from μa to μc. In other words, the measure-preserving property of both the functions f and g is maintained under function composition.
More concisely: If functions f: α -> β and g: β -> γ preserve measures μa and μb, respectively, then their composition g ∘ f preserves the measure from α to γ (μa to μc).
|
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume
theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → α} {s : Set α},
MeasureTheory.MeasurePreserving f μ μ →
MeasurableSet s → ∀ {n : ℕ}, ↑↑μ Set.univ < ↑n * ↑↑μ s → ∃ x ∈ s, ∃ m ∈ Set.Ioo 0 n, f^[m] x ∈ s
This theorem states that if the measure of the universal set is less than `n` times the measure of a set `s` under a measure `μ`, and if `f` is a measure-preserving function, then there exists an element `x` in set `s` and a natural number `m` between 0 and `n` (exclusive) such that the `m`-th iterate of `f` at `x` belongs to `s`.
In other words, if we iterate the function `f`, which preserves the measure, `m` times starting from some point in `s`, we will land back in `s`, for some `m` strictly between 0 and `n`. This is under the condition that the total measure of the space is less than `n` times the measure of `s`. The function `f^[m] x` denotes the `m`-th iterate of `f` at `x`, meaning `f` is applied `m` times.
More concisely: Given a measure-preserving function `f` on a set `s` with measure `μ` in a measurable space of total measure less than `n` times `μ`, there exists an element `x` in `s` and a natural number `m` between 0 and `n-1` such that `f^[m] x` is in `s`.
|
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem
theorem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → α} {s : Set α}
[inst_1 : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.MeasurePreserving f μ μ → MeasurableSet s → ↑↑μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
This theorem states that if we have a self-map that preserves a finite measure, then it will be conservative. More specifically, given a measurable space `α`, a finite measure `μ`, a function `f` that maps `α` to itself, and a measurable set `s`, if the measure `μ` of set `s` is not zero, then there exists at least one point `x` in `s` that, after `m` iterations of applying function `f` (`m` being a non-zero natural number), will return to set `s`. In simpler terms, if we start with a point `x` in `s` and keep applying the function `f`, we will eventually end up back in `s`. This theorem is a particular case of the more general property of measure-preserving transformations being conservative, i.e., almost every point returns to its original set infinitely many times.
More concisely: If `f` is a measure-preserving self-map on the measurable space `(α, Σ, μ)` and `μ(s) > 0`, then there exists an `x ∈ s` such that `f^m(x) ∈ s` for some non-zero `m ∈ ℕ`.
|
MeasureTheory.MeasurePreserving.symm
theorem MeasureTheory.MeasurePreserving.symm :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β)
{μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β},
MeasureTheory.MeasurePreserving (⇑e) μa μb → MeasureTheory.MeasurePreserving (⇑e.symm) μb μa
This theorem states that for any measure-preserving map `e` between two measure spaces `α` and `β`, the inverse map `e.symm` is also measure-preserving. Specifically, if `e` is a measurable equivalence (i.e., a bijective map where both `e` and its inverse are measurable) from `α` to `β`, and if `e` preserves the measure `μa` from `α` to the measure `μb` in `β`, then the inverse map `e.symm` preserves the measure `μb` from `β` to the measure `μa` in `α`.
More concisely: If `e: α → β` is a measure-preserving measurable equivalence, then `e.symm: β → α` is also measure-preserving.
|
MeasureTheory.MeasurePreserving.restrict_preimage_emb
theorem MeasureTheory.MeasurePreserving.restrict_preimage_emb :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β},
MeasureTheory.MeasurePreserving f μa μb →
MeasurableEmbedding f →
∀ (s : Set β), MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
The theorem `MeasureTheory.MeasurePreserving.restrict_preimage_emb` states that, for any types `α` and `β`, given measurable spaces on `α` and `β` (represented as `inst : MeasurableSpace α` and `inst_1 : MeasurableSpace β` respectively), a measure `μa` on `α`, a measure `μb` on `β`, and a function `f` from `α` to `β`, if the function `f` is measure preserving (meaning the measure of any set under the function remains the same) with respect to measures `μa` and `μb`, and if `f` is a measurable embedding (which is a function that is both measurable and injective), then for any set `s` of type `β`, the function `f` is measure preserving with respect to the restriction of `μa` to the preimage of `s` under `f` and the restriction of `μb` to `s`.
In other words, when we restrict our measures to certain sets (the preimage of `s` under `f` for `μa` and `s` for `μb`), the function `f` still preserves the measure.
More concisely: If `f: α → β` is a measure preserving and measurable embedding between measurable spaces `(α, μa)` and `(β, μb)`, then for any set `s ∈ β`, `f` preserves the measures of sets when restricted to the preimage of `s` under `f` for `μa` and `s` for `μb`.
|
MeasureTheory.MeasurePreserving.aemeasurable
theorem MeasureTheory.MeasurePreserving.aemeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β},
MeasureTheory.MeasurePreserving f μa μb → AEMeasurable f μa
This theorem states that for any types `α` and `β`, and any associated measurable spaces `inst` and `inst_1`, along with measures `μa` and `μb` on these spaces, if a function `f` from `α` to `β` preserves the measure (`μa` to `μb`), then `f` is almost everywhere measurable with respect to `μa`. In other words, there exists a measurable function `g` that coincides with `f` almost everywhere (except possibly on a set of measure zero).
More concisely: If `α` and `β` are types with measurable spaces `inst` and `inst_1`, and measures `μa` and `μb`, and `f` is a function from `α` to `β` preserving the measure `μa` to `μb`, then `f` is almost everywhere measurable with respect to `μa`, that is, there exists a measurable function `g` such that `f = g` almost everywhere.
|
MeasureTheory.MeasurePreserving.id
theorem MeasureTheory.MeasurePreserving.id :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α), MeasureTheory.MeasurePreserving id μ μ
This theorem states that for any measurable space `α` and any measure `μ` on that space, the identity function preserves the measure. In other words, applying the identity function to any set in the space does not change its measure under `μ`. In terms of measure theory, it essentially says that the measure of a set remains the same when we do nothing to the set.
More concisely: For any measurable space `(α, Σ, μ)`, the measure of a set `A ∈ Σ` under `μ` is equal to the measure of its identity image `{x ∈ α | x ∈ A}`. In symbols: `μ(A) = μ({x | x ∈ A})`.
|