Dynamical entourages

Bowen-Dinaburg's definition of topological entropy of a transformation T in a metric space (X, d) relies on the so-called dynamical balls. These balls are sets B (x, ε, n) = { y | ∀ k < n, d(T^[k] x, T^[k] y) < ε }.

We implement Bowen-Dinaburg's definitions in the more general context of uniform spaces. Dynamical balls are replaced by what we call dynamical entourages. This file collects all general lemmas about these objects.

Main definitions

• dynEntourage: dynamical entourage associated with a given transformation T, entourage U and time n.

Tags

entropy

TODO

Add product of entourages.

In the context of (pseudo-e)metric spaces, relate the usual definition of dynamical balls with these dynamical entourages.

def Dynamics.dynEntourage {X : Type u_1} (T : X → X) (U : SetRel X X) (n : ℕ) : SetRel X X

The dynamical entourage associated to a transformation T, entourage U and time n is the entourage where x and y are close iff T^[k] x and T^[k] y are U-close for all k < n, i.e. iff they are U-close up to time n.

Equations

• Dynamics.dynEntourage T U n = ⋂ (k : ℕ), ⋂ (_ : k < n), (Prod.map T T)^[k] ⁻¹' U

theorem Dynamics.dynEntourage_eq_inter_Ico {X : Type u_1} (T : X → X) (U : SetRel X X) (n : ℕ) : dynEntourage T U n = ⋂ (k : ↑(Set.Ico 0 n)), (Prod.map T T)^[↑k] ⁻¹' U

theorem Dynamics.mem_dynEntourage {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {x y : X} : (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

theorem Dynamics.mem_ball_dynEntourage {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {x y : X} : y ∈ UniformSpace.ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ UniformSpace.ball (T^[k] x) U

theorem Dynamics.dynEntourage_mem_uniformity {X : Type u_1} {T : X → X} {U : SetRel X X} [UniformSpace X] (h : UniformContinuous T) (U_uni : U ∈ uniformity X) (n : ℕ) : dynEntourage T U n ∈ uniformity X

theorem Dynamics.ball_dynEntourage_mem_nhds {X : Type u_1} {T : X → X} {U : SetRel X X} [UniformSpace X] (h : Continuous T) (U_uni : U ∈ uniformity X) (n : ℕ) (x : X) : UniformSpace.ball x (dynEntourage T U n) ∈ nhds x

instance Dynamics.isRefl_dynEntourage {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} [U.IsRefl] : (dynEntourage T U n).IsRefl

instance Dynamics.isSymm_dynEntourage {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} [U.IsSymm] : (dynEntourage T U n).IsSymm

theorem Dynamics.dynEntourage_comp_subset {X : Type u_1} (T : X → X) (U V : SetRel X X) (n : ℕ) : (dynEntourage T U n).comp (dynEntourage T V n) ⊆ dynEntourage T (U.comp V) n

theorem isOpen.dynEntourage {X : Type u_1} {U : SetRel X X} [TopologicalSpace X] {T : X → X} (T_cont : Continuous T) (U_open : IsOpen U) (n : ℕ) : IsOpen (Dynamics.dynEntourage T U n)

theorem Dynamics.dynEntourage_monotone {X : Type u_1} (T : X → X) (n : ℕ) : Monotone fun (U : SetRel X X) => dynEntourage T U n

theorem Dynamics.dynEntourage_antitone {X : Type u_1} (T : X → X) (U : SetRel X X) : Antitone fun (n : ℕ) => dynEntourage T U n

theorem Dynamics.dynEntourage_mono {X : Type u_1} {T : X → X} {U V : SetRel X X} {m n : ℕ} (hUV : U ⊆ V) (hmn : m ≤ n) : dynEntourage T U n ⊆ dynEntourage T V m

@[simp]

theorem Dynamics.dynEntourage_zero {X : Type u_1} {T : X → X} {U : SetRel X X} : dynEntourage T U 0 = Set.univ

@[simp]

theorem Dynamics.dynEntourage_one {X : Type u_1} {T : X → X} {U : SetRel X X} : dynEntourage T U 1 = U

@[simp]

theorem Dynamics.dynEntourage_univ {X : Type u_1} {T : X → X} {n : ℕ} : dynEntourage T Set.univ n = Set.univ

theorem Dynamics.mem_ball_dynEntourage_comp {X : Type u_1} (T : X → X) (n : ℕ) {U : SetRel X X} [U.IsSymm] (x y : X) (h : (UniformSpace.ball x (dynEntourage T U n) ∩ UniformSpace.ball y (dynEntourage T U n)).Nonempty) : x ∈ UniformSpace.ball y (dynEntourage T (U.comp U) n)

theorem Function.Semiconj.preimage_dynEntourage {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (U : Set (Y × Y)) (n : ℕ) : Prod.map φ φ ⁻¹' Dynamics.dynEntourage T U n = Dynamics.dynEntourage S (Prod.map φ φ ⁻¹' U) n