Documentation

Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

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 #

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.

source
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    instance Dynamics.isRefl_dynEntourage {X : Type u_1} {T : X โ†’ X} {U : SetRel X X} {n : โ„•} [U.IsRefl] :
    (dynEntourage T U n).IsRefl
    source
    ๐Ÿ“ coverage
    instance Dynamics.isSymm_dynEntourage {X : Type u_1} {T : X โ†’ X} {U : SetRel X X} {n : โ„•} [U.IsSymm] :
    (dynEntourage T U n).IsSymm
    source
    ๐Ÿ“ coverage
    @[deprecated Dynamics.isRefl_dynEntourage (since := "2025-10-17")]
    theorem Dynamics.idRel_subset_dynEntourage {X : Type u_1} (T : X โ†’ X) {U : Set (X ร— X)} (h : idRel โŠ† U) (n : โ„•) :
    idRel โŠ† dynEntourage T U n
    source
    ๐Ÿ“ coverage
    @[deprecated Dynamics.isSymm_dynEntourage (since := "2025-10-17")]
    theorem IsSymmetricRel.dynEntourage {X : Type u_1} (T : X โ†’ X) {U : Set (X ร— X)} (h : IsSymmetricRel U) (n : โ„•) :
    IsSymmetricRel (Dynamics.dynEntourage T U n)
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    theorem Dynamics.dynEntourage_monotone {X : Type u_1} (T : X โ†’ X) (n : โ„•) :
    Monotone fun (U : SetRel X X) => dynEntourage T U n
    source
    ๐Ÿ“ coverage
    theorem Dynamics.dynEntourage_antitone {X : Type u_1} (T : X โ†’ X) (U : SetRel X X) :
    Antitone fun (n : โ„•) => dynEntourage T U n
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem Dynamics.dynEntourage_zero {X : Type u_1} {T : X โ†’ X} {U : SetRel X X} :
    dynEntourage T U 0 = Set.univ
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem Dynamics.dynEntourage_one {X : Type u_1} {T : X โ†’ X} {U : SetRel X X} :
    dynEntourage T U 1 = U
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem Dynamics.dynEntourage_univ {X : Type u_1} {T : X โ†’ X} {n : โ„•} :
    dynEntourage T Set.univ n = Set.univ
    source
    ๐Ÿ“ coverage
    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)
    source
    ๐Ÿ“ coverage
    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