Ergodic.ae_empty_or_univ_of_preimage_ae_le'
theorem Ergodic.ae_empty_or_univ_of_preimage_ae_le' :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
Ergodic f μ →
MeasurableSet s →
μ.ae.EventuallyLE (f ⁻¹' s) s → ↑↑μ s ≠ ⊤ → μ.ae.EventuallyEq s ∅ ∨ μ.ae.EventuallyEq s Set.univ
This theorem is titled `Ergodic.ae_empty_or_univ_of_preimage_ae_le'`. It states that for any type `α`, given a measurable space `m` on `α`, a function `f` from `α` to `α`, a set `s` of `α`, and a measure `μ` on `α`, if `f` is ergodic with respect to measure `μ`, and `s` is a measurable set such that the preimage of `s` under `f` is almost everywhere less than or equal to `s` with respect to measure `μ`, and the measure of `s` is not infinite, then almost everywhere with respect to measure `μ`, `s` is equal to the empty set or `s` is equal to the universal set.
In simpler terms, this theorem is exploring the properties of an ergodic function in a measure space. If we have a measurable set and a function that is ergodic with respect to a measure, then under certain conditions, the set is either almost everywhere empty or it is the universal set.
More concisely: In a measurable space with a finite measure, if a measurable set's preimage under an ergodic function is almost everywhere less than or equal to the set itself, then the set is almost everywhere equal to the empty set or the universal set.
|
QuasiErgodic.ae_empty_or_univ₀
theorem QuasiErgodic.ae_empty_or_univ₀ :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
QuasiErgodic f μ →
MeasureTheory.NullMeasurableSet s μ →
μ.ae.EventuallyEq (f ⁻¹' s) s → μ.ae.EventuallyEq s ∅ ∨ μ.ae.EventuallyEq s Set.univ
The theorem `QuasiErgodic.ae_empty_or_univ₀` states that for a quasi-ergodic map (a specific type of transformation in ergodic theory) defined on a measurable space, if we have a set that is almost invariant under the transformation (in the sense of null measurable set), then this set is either almost empty or almost the entire space. "Almost" here refers to the measure of the set in the sense of measure theory: a set is almost empty if the measure of its complement is zero, and a set is almost the entire space if it differs from the entire space by a set of measure zero.
More concisely: A quasi-ergodic map on a measurable space maps almost invariant sets to either almost empty or almost full sets.
|
Ergodic.ae_empty_or_univ_of_ae_le_preimage'
theorem Ergodic.ae_empty_or_univ_of_ae_le_preimage' :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
Ergodic f μ →
MeasurableSet s →
μ.ae.EventuallyLE s (f ⁻¹' s) → ↑↑μ s ≠ ⊤ → μ.ae.EventuallyEq s ∅ ∨ μ.ae.EventuallyEq s Set.univ
This theorem, `Ergodic.ae_empty_or_univ_of_ae_le_preimage'`, states that for any type `α`, measurable space `m` on `α`, function `f` from `α` to `α`, set `s` of `α`, and measure `μ` on the measurable space, if the function `f` is ergodic with respect to the measure `μ`, the set `s` is measurable, the measure of `s` according to the measure `μ` is less than or equal to the preimage of `s` under `f` almost everywhere, and the measure of `s` is not infinite, then the set `s` is eventually equal to the empty set or the universal set almost everywhere with respect to the measure `μ`. This theorem is a part of Ergodic Theory, a branch of mathematics that studies dynamical systems with an invariant measure and related problems.
More concisely: If a function between a measurable space with a finite, ergodic measure is such that the measure of its measurable set is less than or equal to the measure of its preimage almost everywhere, then the set is eventually equal to the empty set or the universal set almost everywhere.
|
QuasiErgodic.ae_empty_or_univ'
theorem QuasiErgodic.ae_empty_or_univ' :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
QuasiErgodic f μ →
MeasurableSet s → μ.ae.EventuallyEq (f ⁻¹' s) s → μ.ae.EventuallyEq s ∅ ∨ μ.ae.EventuallyEq s Set.univ
This theorem is stating that for a quasi ergodic map, any set that is almost invariant (meaning the preimage of the set under the map is almost equal to the set itself) is either almost empty or is almost equal to the universal set. Here, "almost" is in the sense of the filter of co-null sets, or sets of measure zero. This applies to any measurable set in a measurable space, and the map and the measure are both specified as parameters.
More concisely: For any quasi-ergodic map and measurable set in a measurable space, if the set is almost invariant with respect to the map under the measure of co-null sets, then the set is either almost empty or almost equal to the universal set.
|
QuasiErgodic.ae_mem_or_ae_nmem₀
theorem QuasiErgodic.ae_mem_or_ae_nmem₀ :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
QuasiErgodic f μ →
MeasureTheory.NullMeasurableSet s μ →
μ.ae.EventuallyEq (f ⁻¹' s) s → (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s
This theorem states that for a quasi ergodic map, if a set is almost invariant (as opposed to strictly invariant), it is still either almost empty or full with respect to a measure. More specifically, given a measurable space `α`, a map `f` from `α` to `α`, a set `s` of `α`, and a measure `μ` on `α`, if `f` is quasi ergodic with respect to `μ` and `s` is a null measurable set with respect to `μ`, and the preimage of `s` under `f` is almost everywhere equal to `s` with respect to `μ`, then almost everywhere in `α` (with respect to `μ`), an element is either in `s` or not in `s`. This essentially means that quasi ergodic transformations preserve the "almost everywhere" property of sets.
More concisely: Given a quasi ergodic map `f` on a measurable space `(α, μ)`, a null measurable set `s ⊆ α` with almost everywhere equal preimages under `f`, implies that almost everywhere, elements belong to `s` or are disjoint from it.
|
PreErgodic.prob_eq_zero_or_one
theorem PreErgodic.prob_eq_zero_or_one :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α}
[inst : MeasureTheory.IsProbabilityMeasure μ],
PreErgodic f μ → MeasurableSet s → f ⁻¹' s = s → ↑↑μ s = 0 ∨ ↑↑μ s = 1
The theorem `PreErgodic.prob_eq_zero_or_one` states that given a probability space (represented by the type `α`, measurable space `m`, and the probability measure `μ`), a measurable set `s`, and a function `f`, if the ergodic property holds for the function `f` with respect to the measure `μ` (expressed as `PreErgodic f μ`), and if `f` is such that its preimage of `s` equals `s` (expressed as `f ⁻¹' s = s`), then the probability measure of the set `s` (expressed as `↑↑μ s`) is either 0 or 1. This theorem encapsulates the zero-one law of ergodic theory, which essentially states that under the ergodic condition, certain measurable sets can only have extreme probabilities, either 0 or 1.
More concisely: Given a probability space, if a measurable function is ergodic with respect to the measure and maps a measurable set to itself, then the measure of the set is either 0 or 1.
|
Ergodic.ae_empty_or_univ_of_image_ae_le'
theorem Ergodic.ae_empty_or_univ_of_image_ae_le' :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
Ergodic f μ →
MeasurableSet s →
μ.ae.EventuallyLE (f '' s) s → ↑↑μ s ≠ ⊤ → μ.ae.EventuallyEq s ∅ ∨ μ.ae.EventuallyEq s Set.univ
The theorem `Ergodic.ae_empty_or_univ_of_image_ae_le'` states that for any type `α`, measurable space `m`, function `f` from `α` to `α`, set `s` of type `α`, and measure `μ`, if `f` is ergodic with respect to the measure `μ`, the set `s` is measurable, the measure of the image of `s` under `f` is eventually less than or equal to the measure of `s`, and the measure of `s` is not infinite, then the measure of `s` is eventually equal to either the empty set or the universal set. In other words, if a function is ergodic and the measure of the image of a set under the function is not greater than the measure of the original set, then the set must eventually become either empty or the entire space.
More concisely: If a measurable function on a finite measure space is ergodic and maps a measurable set to a set of smaller or equal measure, then the set is eventually a subset of either the empty or the universal set.
|
Ergodic.quasiErgodic
theorem Ergodic.quasiErgodic :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α},
Ergodic f μ → QuasiErgodic f μ
This theorem states that for any type `α`, measurable space `m` defined on `α`, function `f` from `α` to `α`, and measure `μ` on the measurable space, if `f` is an ergodic function with respect to `μ`, then `f` is also quasi-ergodic with respect to `μ`. In the context of measure theory, this theorem essentially describes the relationship between two properties of dynamical systems: ergodicity and quasi-ergodicity, asserting that ergodicity of a map implies its quasi-ergodicity.
More concisely: If `f` is an ergodic function on measurable space `(α, m)` with respect to measure `μ`, then `f` is quasi-ergodic with respect to `μ`.
|