Topological entropy of subsets: monotonicity, closure, union

This file contains general results about the topological entropy of various subsets of the same dynamical system (X, T). We prove that:

• the topological entropy CoverEntropy T F of F is monotone in F: the larger the subset, the larger its entropy.
• the topological entropy of a subset equals the entropy of its closure.
• the entropy of the union of two sets is the maximum of their entropies. We generalize the latter property to finite unions.

Implementation notes

Most results are proved using only the definition of the topological entropy by covers. Some lemmas of general interest are also proved for nets.

TODO

One may implement a notion of Hausdorff convergence for subsets using uniform spaces, and then prove the semicontinuity of the topological entropy. It would be a nice generalization of the lemmas on closures.

Tags

closure, entropy, subset, union

Monotonicity of entropy as a function of the subset

theorem Dynamics.IsDynCoverOf.monotone_subset {X : Type u_1} {T : X → X} {F G : Set X} (F_G : F ⊆ G) {U : Set (X × X)} {n : ℕ} {s : Set X} (h : IsDynCoverOf T G U n s) : IsDynCoverOf T F U n s

theorem Dynamics.IsDynNetIn.monotone_subset {X : Type u_1} {T : X → X} {F G : Set X} (F_G : F ⊆ G) {U : Set (X × X)} {n : ℕ} {s : Set X} (h : IsDynNetIn T F U n s) : IsDynNetIn T G U n s

theorem Dynamics.coverMincard_monotone_subset {X : Type u_1} (T : X → X) (U : Set (X × X)) (n : ℕ) : Monotone fun (F : Set X) => coverMincard T F U n

theorem Dynamics.netMaxcard_monotone_subset {X : Type u_1} (T : X → X) (U : Set (X × X)) (n : ℕ) : Monotone fun (F : Set X) => netMaxcard T F U n

theorem Dynamics.coverEntropyInfEntourage_monotone {X : Type u_1} (T : X → X) (U : Set (X × X)) : Monotone fun (F : Set X) => coverEntropyInfEntourage T F U

theorem Dynamics.coverEntropyEntourage_monotone {X : Type u_1} (T : X → X) (U : Set (X × X)) : Monotone fun (F : Set X) => coverEntropyEntourage T F U

theorem Dynamics.netEntropyInfEntourage_monotone {X : Type u_1} (T : X → X) (U : Set (X × X)) : Monotone fun (F : Set X) => netEntropyInfEntourage T F U

theorem Dynamics.netEntropyEntourage_monotone {X : Type u_1} (T : X → X) (U : Set (X × X)) : Monotone fun (F : Set X) => netEntropyEntourage T F U

theorem Dynamics.coverEntropyInf_monotone {X : Type u_1} [UniformSpace X] (T : X → X) : Monotone fun (F : Set X) => coverEntropyInf T F

theorem Dynamics.coverEntropy_monotone {X : Type u_1} [UniformSpace X] (T : X → X) : Monotone fun (F : Set X) => coverEntropy T F

Closure

theorem Dynamics.IsDynCoverOf.closure {X : Type u_1} [UniformSpace X] {T : X → X} (h : Continuous T) {F : Set X} {U V : Set (X × X)} (V_uni : V ∈ uniformity X) {n : ℕ} {s : Set X} (s_cover : IsDynCoverOf T F U n s) : IsDynCoverOf T (_root_.closure F) (compRel U V) n s

theorem Dynamics.coverMincard_closure_le {X : Type u_1} [UniformSpace X] {T : X → X} (h : Continuous T) (F : Set X) (U : Set (X × X)) {V : Set (X × X)} (V_uni : V ∈ uniformity X) (n : ℕ) : coverMincard T (closure F) (compRel U V) n ≤ coverMincard T F U n

theorem Dynamics.coverEntropyInfEntourage_closure {X : Type u_1} [UniformSpace X] {T : X → X} (h : Continuous T) (F : Set X) (U : Set (X × X)) {V : Set (X × X)} (V_uni : V ∈ uniformity X) : coverEntropyInfEntourage T (closure F) (compRel U V) ≤ coverEntropyInfEntourage T F U

theorem Dynamics.coverEntropyEntourage_closure {X : Type u_1} [UniformSpace X] {T : X → X} (h : Continuous T) (F : Set X) (U : Set (X × X)) {V : Set (X × X)} (V_uni : V ∈ uniformity X) : coverEntropyEntourage T (closure F) (compRel U V) ≤ coverEntropyEntourage T F U

theorem Dynamics.coverEntropyInf_closure {X : Type u_1} [UniformSpace X] {T : X → X} (h : Continuous T) {F : Set X} : coverEntropyInf T (closure F) = coverEntropyInf T F

theorem Dynamics.coverEntropy_closure {X : Type u_1} [UniformSpace X] {T : X → X} (h : Continuous T) {F : Set X} : coverEntropy T (closure F) = coverEntropy T F

Finite unions

theorem Dynamics.IsDynCoverOf.union {X : Type u_1} {T : X → X} {F G : Set X} {U : Set (X × X)} {n : ℕ} {s t : Set X} (hs : IsDynCoverOf T F U n s) (ht : IsDynCoverOf T G U n t) : IsDynCoverOf T (F ∪ G) U n (s ∪ t)

theorem Dynamics.coverMincard_union_le {X : Type u_1} (T : X → X) (F G : Set X) (U : Set (X × X)) (n : ℕ) : coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

theorem Dynamics.coverEntropyEntourage_union {X : Type u_1} {T : X → X} {F G : Set X} {U : Set (X × X)} : coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

theorem Dynamics.coverEntropy_union {X : Type u_1} [UniformSpace X] {T : X → X} {F G : Set X} : coverEntropy T (F ∪ G) = max (coverEntropy T F) (coverEntropy T G)

theorem Dynamics.coverEntropyInf_iUnion_le {X : Type u_1} {ι : Type u_2} [UniformSpace X] (T : X → X) (F : ι → Set X) : ⨆ (i : ι), coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ (i : ι), F i)

theorem Dynamics.coverEntropy_iUnion_le {X : Type u_1} {ι : Type u_2} [UniformSpace X] (T : X → X) (F : ι → Set X) : ⨆ (i : ι), coverEntropy T (F i) ≤ coverEntropy T (⋃ (i : ι), F i)

theorem Dynamics.coverEntropyInf_biUnion_le {X : Type u_1} {ι : Type u_2} [UniformSpace X] (s : Set ι) (T : X → X) (F : ι → Set X) : ⨆ i ∈ s, coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ i ∈ s, F i)

theorem Dynamics.coverEntropy_biUnion_le {X : Type u_1} {ι : Type u_2} [UniformSpace X] (s : Set ι) (T : X → X) (F : ι → Set X) : ⨆ i ∈ s, coverEntropy T (F i) ≤ coverEntropy T (⋃ i ∈ s, F i)

noncomputable def Dynamics.coverEntropy_supBotHom {X : Type u_1} [UniformSpace X] (T : X → X) : SupBotHom (Set X) EReal

Topological entropy CoverEntropy T as a SupBotHom function of the subset.

Equations

• Dynamics.coverEntropy_supBotHom T = { toFun := Dynamics.coverEntropy T, map_sup' := ⋯, map_bot' := ⋯ }

theorem Dynamics.coverEntropy_iUnion_of_finite {X : Type u_1} {ι : Type u_2} [UniformSpace X] [Finite ι] {T : X → X} {F : ι → Set X} : coverEntropy T (⋃ (i : ι), F i) = ⨆ (i : ι), coverEntropy T (F i)

theorem Dynamics.coverEntropy_biUnion_finset {X : Type u_1} {ι : Type u_2} [UniformSpace X] {T : X → X} {F : ι → Set X} {s : Finset ι} : coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)