PreErgodic.ae_eq_const_of_ae_eq_comp
theorem PreErgodic.ae_eq_const_of_ae_eq_comp :
∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Nonempty X]
[inst_2 : MeasurableSpace X] [inst_3 : HasCountableSeparatingOn X MeasurableSet Set.univ] {f : α → α} {g : α → X},
PreErgodic f μ → Measurable g → g ∘ f = g → ∃ c, μ.ae.EventuallyEq g (Function.const α c)
The theorem states that for a system represented by a pre-ergodic map `f` mapping a measurable space 'α' to itself, and `g` is a measurable function from 'α' to another nonempty measurable space 'X' that has a countable family of measurable sets separating the points of 'X'. If the function `g` remains unchanged under the application of `f` (i.e., `g` is invariant under `f`), then `g` is almost everywhere (a.e.) constant. In other words, there exists a constant 'c' such that `g` is equal to this constant almost everywhere in the measure space 'α', with respect to a given measure 'μ'.
This theorem is crucial in ergodic theory, a branch of mathematics that studies dynamical systems with an invariant measure, and it essentially implies that for such a system, any invariant measurable function must be constant almost everywhere.
More concisely: If a measurable function `g` from a pre-ergodic measure space `(α, μ)` with a countable separation property, is invariant under a measurable map `f`: `g ∘ f = g`, then `g` is almost everywhere constant.
|
QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀
theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀ :
∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Nonempty X]
[inst_2 : MeasurableSpace X] {s : Set X} [inst_3 : HasCountableSeparatingOn X MeasurableSet s] {f : α → α}
{g : α → X},
QuasiErgodic f μ →
(∀ᵐ (x : α) ∂μ, g x ∈ s) →
MeasureTheory.NullMeasurable g μ →
μ.ae.EventuallyEq (g ∘ f) g → ∃ c, μ.ae.EventuallyEq g (Function.const α c)
The theorem `QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀` states the following:
Let `f` be a function from a measurable space `α` to itself that is (quasi)ergodic. Suppose `g` is a null-measurable function from `α` to another nonempty space `X`, and there exists a countable family of measurable sets in `X` that separates points of a set `s` such that for almost every point `x` in `α`, `f(x)` belongs to `s`. If function `g` is almost everywhere invariant under `f`, meaning the composition of `g` and `f` is equal to `g` almost everywhere, then `g` is almost everywhere constant. In other words, there exists a constant `c` such that `g(x)` equals `c` for almost every `x` in `α`.
More concisely: If a (quasi)ergodic function maps almost every point in a measurable space to a set where a null-measurable function is almost everywhere invariant, then that function is almost everywhere constant.
|
Ergodic.ae_eq_const_of_ae_eq_comp₀
theorem Ergodic.ae_eq_const_of_ae_eq_comp₀ :
∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Nonempty X]
[inst_2 : MeasurableSpace X] [inst_3 : HasCountableSeparatingOn X MeasurableSet Set.univ] {f : α → α} {g : α → X},
Ergodic f μ →
MeasureTheory.NullMeasurable g μ →
μ.ae.EventuallyEq (g ∘ f) g → ∃ c, μ.ae.EventuallyEq g (Function.const α c)
This theorem states that for an ergodic map `f` from a set `α` to itself, and a null-measurable function `g` from `α` to a nonempty measurable space `X` that has a countable family of measurable sets separating the points in `X`, if `g` is almost everywhere (a.e.) invariant under the application of `f` (i.e., the function `g` applied to `f` is equal to `g` almost everywhere), then there exists a constant `c` such that `g` equals this constant function almost everywhere. In other words, under these conditions, the function `g` is almost everywhere constant.
More concisely: For an ergodic map `f` on a measurable set `α` and a null-measurable, a.e. `f`-invariant function `g` from `α` to a separable measurable space `X`, there exists a constant `c` such that `g = const c` a.e. on `α`.
|
QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae
theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae :
∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace.MetrizableSpace X] [inst_3 : Nonempty X] {f : α → α}
{g : α → X},
QuasiErgodic f μ →
MeasureTheory.AEStronglyMeasurable g μ →
μ.ae.EventuallyEq (g ∘ f) g → ∃ c, μ.ae.EventuallyEq g (Function.const α c)
The theorem states that for a quasi ergodic map `f : α → α`, and a function `g : α → X` which is almost everywhere strongly measurable with respect to a measure `μ` and maps from `α` to a nonempty metrizable topological space, if `g` is almost everywhere-invariant under the operation of `f`, then `g` is almost everywhere constant. In mathematical terms, if `f` is a quasi ergodic map, `g` is a function that is strongly measurable almost everywhere, and `g(f(x))` is almost everywhere equal to `g(x)`, then there exists a constant `c` such that `g(x)` is almost everywhere equal to `c`.
More concisely: If a quasi-ergodic map `f` and a strongly measurable almost everywhere function `g : α → X` are almost everywhere invariant with each other, then `g` is almost everywhere constant.
|
QuasiErgodic.ae_eq_const_of_ae_eq_comp₀
theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp₀ :
∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Nonempty X]
[inst_2 : MeasurableSpace X] [inst_3 : HasCountableSeparatingOn X MeasurableSet Set.univ] {f : α → α} {g : α → X},
QuasiErgodic f μ →
MeasureTheory.NullMeasurable g μ →
μ.ae.EventuallyEq (g ∘ f) g → ∃ c, μ.ae.EventuallyEq g (Function.const α c)
This theorem states that given `f` which is a quasi ergodic map on a measurable space `α`, and `g` which is a null-measurable function from `α` to a nonempty measurable space `X` with a countable family of measurable sets separating the points of `X`, if `g` is almost everywhere invariant under `f`, then `g` is almost everywhere constant. In other words, under these conditions, there exists some constant `c` such that `g` is equal to `c` almost everywhere.
More concisely: If `f` is a quasi-ergodic map on the measurable space `α`, and `g` is a null-measurable, almost everywhere invariant function from `α` to a separable measurable space `X`, then `g` is almost everywhere constant.
|
Ergodic.ae_eq_const_of_ae_eq_comp_ae
theorem Ergodic.ae_eq_const_of_ae_eq_comp_ae :
∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace.MetrizableSpace X] [inst_3 : Nonempty X] {f : α → α}
{g : α → X},
Ergodic f μ →
MeasureTheory.AEStronglyMeasurable g μ →
μ.ae.EventuallyEq (g ∘ f) g → ∃ c, μ.ae.EventuallyEq g (Function.const α c)
Let `f : α → α` be a map that is ergodic with respect to a measure `μ`, and let `g : α → X` be a function that is almost everywhere strongly measurable with respect to the same measure, where `X` is a nonempty metrizable topological space. If the function `g` is almost everywhere invariant under the map `f`, that is, if almost everywhere we have `g(f(x)) = g(x)`, then the function `g` is almost everywhere constant. In other words, there exists a value `c` such that `g(x) = c` almost everywhere.
More concisely: If a map `f` is ergodic with respect to a measure `μ`, and a strongly measurable function `g : α → X` is almost everywhere invariant under `f`, then `g` is almost everywhere constant.
|