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

Once #PR14718 has passed, 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 : Set (X × X)) (n : ℕ) : Set (X × X)

The dynamical entourage associated to a transformation T, entourage U and time n is the set of points (x, y) such that (T^[k] x, T^[k] y) ∈ U for all k < n, i.e. which 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 : Set (X × X)) (n : ℕ) : Dynamics.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 : Set (X × X)} {n : ℕ} {x : X} {y : X} : (x, y) ∈ Dynamics.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 : Set (X × X)} {n : ℕ} {x : X} {y : X} : y ∈ UniformSpace.ball x (Dynamics.dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ UniformSpace.ball (T^[k] x) U

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

theorem Dynamics.idRel_subset_dynEntourage {X : Type u_1} (T : X → X) {U : Set (X × X)} (h : idRel ⊆ U) (n : ℕ) : idRel ⊆ Dynamics.dynEntourage T U n

theorem SymmetricRel.dynEntourage {X : Type u_1} (T : X → X) {U : Set (X × X)} (h : SymmetricRel U) (n : ℕ) : SymmetricRel (Dynamics.dynEntourage T U n)

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

theorem isOpen.dynEntourage {X : Type u_1} [TopologicalSpace X] {T : X → X} (T_cont : Continuous T) {U : Set (X × X)} (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 : Set (X × X)) => Dynamics.dynEntourage T U n

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

@[simp]

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

@[simp]

theorem Dynamics.dynEntourage_one {X : Type u_1} {T : X → X} {U : Set (X × X)} : Dynamics.dynEntourage T U 1 = U

@[simp]

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

theorem Dynamics.mem_ball_dynEntourage_comp {X : Type u_1} (T : X → X) (n : ℕ) {U : Set (X × X)} (U_symm : SymmetricRel U) (x : X) (y : X) (h : (UniformSpace.ball x (Dynamics.dynEntourage T U n) ∩ UniformSpace.ball y (Dynamics.dynEntourage T U n)).Nonempty) : x ∈ UniformSpace.ball y (Dynamics.dynEntourage T (compRel U U) n)

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