uniformEquicontinuous_birkhoffAverage
theorem uniformEquicontinuous_birkhoffAverage :
∀ (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : RCLike 𝕜]
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : X → X} {g : X → E},
LipschitzWith 1 f → UniformContinuous g → UniformEquicontinuous (birkhoffAverage 𝕜 f g)
The theorem `uniformEquicontinuous_birkhoffAverage` asserts the following: for any type `𝕜`, and types `X` and `E` with `X` a pseudo emetric space, `𝕜` a real-like number system, and `E` a normed additive commutative group that is a normed space over `𝕜`, if `f` is a function from `X` to `X` that is Lipschitz continuous with constant `1` (i.e., for any `x, y` in `X`, the distance between `f(x)` and `f(y)` is less than or equal to the distance between `x` and `y`) and `g` is a function from `X` to `E` that is uniformly continuous (i.e., if `x` and `y` in `X` are sufficiently close, then `g(x)` and `g(y)` are close regardless of the actual values of `x` and `y`), then the Birkhoff averages of `g` along orbits of `f` form a uniformly equicontinuous family of functions. A family of functions is uniformly equicontinuous if, for any given closeness criteria in the output space, there exists a closeness criteria in the input space such that if any two inputs are close according to this criteria, then their outputs via any function in the family will be close according to the given output closeness criteria.
More concisely: Given a pseudo metric space `X`, a real-number system `𝕜`, a normed additive commutative group `E` over `𝕜`, a Lipschitz continuous function `f: X → X`, and a uniformly continuous function `g: X → E`, the Birkhoff averages of `g` along orbits of `f` form a uniformly equicontinuous family.
|
tendsto_birkhoffAverage_apply_sub_birkhoffAverage'
theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage' :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
[inst_2 : Module 𝕜 E] [inst_3 : BoundedSMul 𝕜 E] {g : α → E},
Bornology.IsBounded (Set.range g) →
∀ (f : α → α) (x : α),
Filter.Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (nhds 0)
This theorem states that if a function `g` mapping from some type `α` to a normed additive commutative group `E`, which is also a module over a real-like field `𝕜`, is bounded (meaning the set of all outputs of `g` is bounded), then for any transformation `f` on `α` and any point `x` in `α`, the difference between the Birkhoff averages of `g` along the orbit of `f(x)` and along the orbit of `x` will tend to zero as the number of terms in the average goes to infinity.
In mathematical terms, if `g` is bounded, then for any `f : α → α` and any `x : α`, we have that the sequence `birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x` tends to zero as `n → ∞`, where `birkhoffAverage 𝕜 f g n x` represents the Birkhoff average of `g` along the first `n` terms of the orbit of `x` under `f`.
This theorem is a statement about the convergence properties of Birkhoff averages in dynamical systems, showing that under certain conditions, the Birkhoff averages along different orbits will eventually become arbitrarily close.
More concisely: If `g : α -> E` is a bounded function from a set `α` to a normed additive commutative group `E` over a real-like field `𝕜`, then the difference between the Birkhoff averages of `g` along the orbits of any point `x` under a transformation `f : α -> α` tends to zero as the number of terms in the average goes to infinity.
|
tendsto_birkhoffAverage_apply_sub_birkhoffAverage
theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
[inst_2 : Module 𝕜 E] [inst_3 : BoundedSMul 𝕜 E] {f : α → α} {g : α → E} {x : α},
Bornology.IsBounded (Set.range fun x_1 => g (f^[x_1] x)) →
Filter.Tendsto (fun n => birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) Filter.atTop (nhds 0)
This theorem states that for any types `α` and `E`, where `E` is a normed additive commutative group, and any type `𝕜` which behaves like a real closed field and for which `E` is a `𝕜`-module and bounded semimultiplicative, given a function `f` from `α` to `α`, a function `g` from `α` to `E`, and an element `x` of `α`, if the function `g` is bounded along the orbit of `x` under `f` (i.e., the set of all points obtained by repeatedly applying `f` to `x` is bounded), then the difference between the Birkhoff averages of `g` along the orbit of `f(x)` and along the orbit of `x` tends to zero as the number of terms in the average goes to infinity. The Birkhoff average of a function `g` along an orbit is the average value of `g` over the orbit, and this theorem essentially says that the average behavior of `g` on the orbits of `x` and `f(x)` becomes increasingly similar as we look at more and more terms.
More concisely: Given a normed additive commutative group `E`, a real closed field `𝕜`, an `𝕜`-module and bounded semimultiplicative `E`, a function `f: α -> α`, a function `g: α -> E`, and an element `x in α` such that `g` is bounded along the orbit of `x` under `f`, the Birkhoff averages of `g` along the orbits of `x` and `f(x)` converge to the same limit as the number of terms approaches infinity.
|
Function.IsFixedPt.tendsto_birkhoffAverage
theorem Function.IsFixedPt.tendsto_birkhoffAverage :
∀ {α : Type u_1} {E : Type u_2} (R : Type u_3) [inst : DivisionSemiring R] [inst_1 : CharZero R]
[inst_2 : AddCommMonoid E] [inst_3 : TopologicalSpace E] [inst_4 : Module R E] {f : α → α} {x : α},
Function.IsFixedPt f x →
∀ (g : α → E), Filter.Tendsto (fun x_1 => birkhoffAverage R f g x_1 x) Filter.atTop (nhds (g x))
This theorem, named `Function.IsFixedPt.tendsto_birkhoffAverage`, states that for a fixed point `x` of a function `f` mapping `α → α`, the Birkhoff averages of another function `g` that maps `α → E` over the orbit of `x` tend to `g(x)` as `N` tends to infinity. Here, `α`, `E`, and `R` are types, with `R` being a division semiring with no zero divisors. `E` is a type with a topology and is a module over `R`. The Birkhoff averages are actually equal to `g(x)` for all `N ≠ 0`, which is stated in `Function.IsFixedPt.birkhoffAverage_eq`. A future enhancement may include a version for a periodic orbit.
More concisely: For a fixed point `x` of a function `f` from type `α` to itself, and a function `g` from `α` to a topological space `E` over a division semiring `R` with no zero divisors, the Birkhoff averages of `g` over the orbit of `x` converge to `g(x)` as the number of iterations `N` approaches infinity.
|
isClosed_setOf_tendsto_birkhoffAverage
theorem isClosed_setOf_tendsto_birkhoffAverage :
∀ (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : RCLike 𝕜]
[inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : X → X} {g l : X → E},
LipschitzWith 1 f →
UniformContinuous g →
Continuous l →
IsClosed {x | Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 f g x_1 x) Filter.atTop (nhds (l x))}
This theorem states that if we have a non-strictly contracting map `f : X → X`, which means that it is Lipschitz continuous with a constant `1`, and two functions `g : X → E` and `l : X → E` where `g` is uniformly continuous and `l` is continuous, then the set of all points `x` such that the Birkhoff average of `g` along the orbit of `x` tends to `l x`, forms a closed set. Here, the Birkhoff average of `g` along the orbit of `x` is described by the function `(fun x_1 => birkhoffAverage 𝕜 f g x_1 x)`, which is assumed to tend towards `l x` as `x_1` goes to infinity (as expressed by `Filter.Tendsto ... Filter.atTop (nhds (l x))`). This is formalized in Lean 4 as `IsClosed {x | Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 f g x_1 x) Filter.atTop (nhds (l x))}`.
More concisely: If `f : X -> X` is a non-strictly contracting map, `g : X -> E` is uniformly continuous, `l : X -> E` is continuous, and the Birkhoff averages of `g` along the orbits of `x` tend to `l x` as `x_1` goes to infinity, then the set of `x` such that this convergence holds is closed.
|