MeasureTheory.Conservative.exists_mem_iterate_mem
theorem MeasureTheory.Conservative.exists_mem_iterate_mem :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ → ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
The theorem `MeasureTheory.Conservative.exists_mem_iterate_mem` states that for any measurable space `α`, any function `f` mapping `α` to `α`, and any measure `μ` on `α`, if `f` is a conservative self-map and `s` is a measurable set in `α` with non-zero measure, then there exists an element `x` in `s` such that `x` returns to `s` after a non-zero number of iterations of `f`. In other words, applying `f` a non-zero number of times to `x` will result in a value that is also in `s`.
More concisely: For any measurable space `α`, measurable set `s` with non-zero measure, and conservative self-map `f` on `α`, there exists an element `x` in `s` such that `f^n(x)` is in `s` for some non-zero natural number `n`.
|
MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem
theorem MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ →
MeasurableSet s → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
The Poincaré Recurrence Theorem in measure theory states that, for any given conservative map `f`, a measurable space `α`, a measurable set `s` within this space, and a measure `μ` over the space, if almost every point `x` in `s` is conserved under `f` with respect to measure `μ`, then for almost every point `x` in `s`, there exist infinite natural numbers `n` such that the `n`-th iterate of `f` at `x` is in `s`. The term "almost every" is in the measure-theoretic sense, meaning that the set of points for which the property does not hold has measure zero. The `Filter.atTop` represents the limit going to infinity in the set of natural numbers. This theorem is a fundamental result in ergodic theory, providing conditions under which points in a set will repeatedly return to the set.
More concisely: If a measurable set contains almost every point of zero-measure recurrent points under a conservative map in a measure space, then for almost every point in the set, there exist infinitely many iterates that lie within the set.
|
MeasureTheory.Conservative.id
theorem MeasureTheory.Conservative.id :
∀ {α : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α), MeasureTheory.Conservative id μ := by
sorry
This theorem states that for any type `α` and any measurable space over `α`, any measure `μ` is conservative with respect to the identity map. In the context of measure theory, a measure is said to be conservative if, roughly speaking, it does not "lose mass" under the application of the function. In this case, the function is the identity function, which does not change its input, so intuitively any measure should be conservative with respect to it.
More concisely: For any measurable space and measure over a type `α`, the identity function is measure-preserving, that is, it preserves the measure of sets.
|
MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero
theorem MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ → MeasurableSet s → ↑↑μ s ≠ 0 → ∀ (N : ℕ), ∃ m > N, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
This theorem states that given a conservative map `f` and a measurable set `s` of nonzero measure in a measurable space `α` with measure `μ`, if you iterate the map `f` an arbitrarily large number of times `m` (greater than any given natural number `N`), you can always find a set of points `x` in `s` that returns back to `s` after `m` iterations of `f` and this set of points has nonzero measure.
In other words, for any conservative system (described by the map `f`), and any set `s` with nonzero measure, there will always be points in `s` that eventually return to `s` after some high enough number of applications of the map, and the measure of such points is always nonzero.
This theorem is significant in the study of dynamical systems where conservative maps are used to model systems that preserve a certain measure (like physical systems conserving energy).
More concisely: Given a conservative map `f` and a measurable set `s` of nonzero measure in a measurable space with measure `μ`, there exists a subset of points in `s` that returns to `s` after some arbitrarily large number of iterations of `f`, and this subset has nonzero measure.
|
MeasureTheory.MeasurePreserving.conservative
theorem MeasureTheory.MeasurePreserving.conservative :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α}
[inst_1 : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.MeasurePreserving f μ μ → MeasureTheory.Conservative f μ
This theorem states that, for any given type `α` with a measurable space structure, a function `f` from `α` to `α`, and a finite measure `μ` on `α`, if `f` is a measure-preserving function with respect to `μ`, then `f` is conservative. In the context of measure theory, a function is conservative if for every set with positive measure, there is a positive integer `n` such that the `n`-fold iterate of the function has positive measure on this set.
More concisely: If `α` is a type with a measurable space structure, `f: α → α` is a measure-preserving function with respect to finite measure `μ` on `α`, then `f` is conservative.
|
MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds
theorem MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds :
∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : SecondCountableTopology α]
[inst_3 : OpensMeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ → ∀ᵐ (x : α) ∂μ, ∀ s ∈ nhds x, ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
The theorem is known as the Poincaré recurrence theorem. It states that for a conservative dynamical system `f : α → α` operating on a topological space that has a second countable topology and measurable open sets, almost every point `x : α` is recurrent. In other words, almost every point visits every neighborhood `s ∈ 𝓝 x` infinitely many times. Here, a neighborhood of `x` is defined as a set that contains an open set around `x`. The theorem uses the measure `μ` to specify "almost every" point, and the neighborhood filter at `x`, `nhds x`, to define the neighborhoods of `x`. The statement `∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s` means that there exists a natural number `n` such that for all `m ≥ n`, the `m-th` iterate of `f` at `x` is in `s`. In simpler terms, it means that the point `x` returns to the neighborhood `s` infinitely often. The filter `Filter.atTop` represents the limit as `n` goes to infinity.
More concisely: In a conservative dynamical system on a second countable topological space with measurable open sets, almost every point recurrently visits every neighborhood infinitely many times.
|
MeasureTheory.Conservative.frequently_measure_inter_ne_zero
theorem MeasureTheory.Conservative.frequently_measure_inter_ne_zero :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ →
MeasurableSet s → ↑↑μ s ≠ 0 → ∃ᶠ (m : ℕ) in Filter.atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
This theorem states that, given a measurable space `α`, a function `f` from `α` to `α`, a set `s` of `α`, and a measure `μ` on `α`, if `f` is a conservative map and `s` is a measurable set with non-zero measure, then there are infinitely many natural numbers `m` such that the measure of the intersection of `s` and the preimage of `s` under `m` iterations of `f` is not zero. This essentially means that for a large number of `m`, a positive measure of points in `s` returns back to `s` after `m` iterations of `f`. The collection of such `m` is described by the filter `Filter.atTop`, which represents a limit towards infinity.
More concisely: Given a measurable space `α`, a measurable set `s` with non-zero measure, a conservative function `f` from `α` to `α`, there exists a filter `F` of natural numbers such that for all `m` in `F`, the measure of `s ∩ f^m(s)` is positive.
|
MeasureTheory.Conservative.ae_forall_image_mem_imp_frequently_image_mem
theorem MeasureTheory.Conservative.ae_forall_image_mem_imp_frequently_image_mem :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ →
MeasurableSet s → ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
This is a formulation of the Poincaré recurrence theorem in the context of measure theory and dynamical systems. The theorem states that for any measure-theoretic dynamical system `f`, and any measurable set `s`, if a point `x` in the space (almost everywhere with respect to the measure `μ`) has its orbit under `f` intersect `s` at least once (i.e., for some natural number `k`, the `k`-th iterate of `f` applied to `x` is in `s`), then the orbit of `x` will intersect `s` infinitely many times. This is symbolically represented as there being frequently (in the formal sense of 'eventually and frequently' pertaining to filters) a natural number `n` such that the `n`-th iterate of `f` applied to `x` is in `s`. The precondition for this is that `f` needs to be a conservative dynamical system with respect to the measure `μ`.
More concisely: In the context of measure theory and dynamical systems, if a point `x` in a measure space has its orbit intersect a measurable set `s` at least once under a conservative dynamical system `f` (with respect to the measure `μ`), then `x`'s orbit intersects `s` infinitely many times.
|
MeasureTheory.Conservative.measure_mem_forall_ge_image_not_mem_eq_zero
theorem MeasureTheory.Conservative.measure_mem_forall_ge_image_not_mem_eq_zero :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ → MeasurableSet s → ∀ (n : ℕ), ↑↑μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
The Poincaré recurrence theorem asserts that for any measure space `α`, a conservative map `f` mapping `α` to itself, a measurable set `s` of elements of `α`, and a measure `μ` on `α`, if `f` is conservative and `s` is a measurable set, then the measure of the set of points `x` in `s` such that `x` does not return to `s` after `n` or more iterations of the map `f` is zero for any natural number `n`. In simple terms, almost all points in a measurable set under a conservative dynamic system will eventually return to the set after a sufficient number of iterations.
More concisely: For any conservative map `f` on a measure space `(α, μ)` and measurable set `s`, the measure of points in `s` that do not return to `s` after infinitely many iterations is zero.
|
MeasureTheory.Conservative.iterate
theorem MeasureTheory.Conservative.iterate :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ → ∀ (n : ℕ), MeasureTheory.Conservative f^[n] μ
This theorem states that for any natural number `n`, the `n`th iteration of a conservative system is also a conservative system. In more detail, given a measurable space `α`, a function `f : α → α`, and a measure `μ`, if the function `f` with the measure `μ` forms a conservative system, then the `n`th iterative application of the function `f` (denoted by `f^[n]`) with the same measure `μ` also forms a conservative system.
More concisely: For any measurable space `α`, function `f : α → α`, and measure `μ`, if `(f, μ)` is a conservative system, then `(f^[n], μ)` is also a conservative system for any natural number `n`.
|
MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem
theorem MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem :
∀ {α : Type u_2} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
MeasureTheory.Conservative f μ →
MeasurableSet s → ↑↑μ s ≠ 0 → ∃ᵐ (x : α) ∂μ, x ∈ s ∧ ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s
The theorem states that if `f` is a conservative self-map (i.e., a map from a set to itself which preserves some structure or property) and `s` is a measurable set with positive measure (i.e., the size of the set is positive, in a sense appropriate to the measure space), then almost everywhere (except for a set of measure zero) in the measure space, we can find an element `x` in `s` such that, under infinitely many iterations of the map `f`, `x` still returns to the set `s`.
In mathematical terms, for almost all `x` in the measure space, `x` belongs to `s` and there are infinitely many natural numbers `n` such that the `n`-th iterate of `f` applied to `x` also belongs to `s`. This limit behavior is captured by the 'at top' filter, which considers the limit as `n` goes to infinity.
More concisely: Given a conservative self-map `f` on a measure space and a measurable set `s` of positive measure, almost every element `x` in `s` belongs to `s` under infinitely many iterations of `f` according to the 'at top' filter.
|