Topological entropy via covers

We implement Bowen-Dinaburg's definitions of the topological entropy, via covers.

All is stated in the vocabulary of uniform spaces. For compact spaces, the uniform structure is canonical, so the topological entropy depends only on the topological structure. This will give a clean proof that the topological entropy is a topological invariant of the dynamics.

A notable choice is that we define the topological entropy of a subset F of the whole space. Usually, one defines the entropy of an invariant subset F as the entropy of the restriction of the transformation to F. We avoid the latter definition as it would involve frequent manipulation of subtypes. Our version directly gives a meaning to the topological entropy of a subsystem, and a single theorem (subset_restriction_entropy in TopologicalEntropy.Morphism) will give the equivalence between both versions.

Another choice is to give a meaning to the entropy of ∅ (it must be -∞ to stay coherent) and to keep the possibility for the entropy to be infinite. Hence, the entropy takes values in the extended reals [-∞, +∞]. The consequence is that we use ℕ∞, ℝ≥0∞ and EReal numbers.

Main definitions

• IsDynCoverOf: property that dynamical balls centered on a subset s cover a subset F.
• coverMincard: minimal cardinal of a dynamical cover. Takes values in ℕ∞.
• coverEntropyInfEnt/coverEntropyEnt: exponential growth of coverMincard. The former is defined with a liminf, the later with a limsup. Take values in EReal.
• coverEntropyInf/coverEntropy: supremum of coverEntropyInfEnt/coverEntropyEnt over all entourages (or limit as the entourages go to the diagonal). These are Bowen-Dinaburg's versions of the topological entropy with covers. Take values in EReal.

Implementation notes

There are two competing definitions of topological entropy in this file: one uses a liminf, the other a limsup. These two topological entropies are equal as soon as they are applied to an invariant subset by theorem coverEntropyInf_eq_coverEntropy. We choose the default definition to be the definition using a limsup, and give it the simpler name coverEntropy (instead of coverEntropySup). Theorems about the topological entropy of invariant subsets will be stated using only coverEntropy.

Main results

• IsDynCoverOf.iterate_le_pow: given a dynamical cover at time n, creates dynamical covers at all iterates n * m with controlled cardinality.
• IsDynCoverOf.coverEntropyEnt_le_log_card_div: upper bound on coverEntropyEnt given any dynamical cover.
• coverEntropyInf_eq_coverEntropy: equality between the notions of topological entropy defined with a liminf and a limsup.

Tags

cover, entropy

TODO

The most painful part of many manipulations involving topological entropy is going from coverMincard to coverEntropyInfEnt/coverEntropyEnt. It involves a logarithm, a division, a liminf/limsup, and multiple coercions. The best thing to do would be to write a file on "exponential growth" to make a clean pathway from estimates on coverMincard to estimates on coverEntropyInf/coverEntropy. It would also be useful in other similar contexts, including the definition of entropy using nets.

Get versions of the topological entropy on (pseudo-e)metric spaces.

Dynamical covers

def Dynamics.IsDynCoverOf {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) (s : Set X) : Prop

Given a subset F, an entourage U and an integer n, a subset s is a (U, n)- dynamical cover of F if any orbit of length n in F is U-shadowed by an orbit of length n of a point in s.

Equations

• Dynamics.IsDynCoverOf T F U n s = (F ⊆ ⋃ x ∈ s, UniformSpace.ball x (Dynamics.dynEntourage T U n))

theorem Dynamics.IsDynCoverOf.of_le {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} {m : ℕ} {n : ℕ} (m_n : m ≤ n) {s : Set X} (h : Dynamics.IsDynCoverOf T F U n s) : Dynamics.IsDynCoverOf T F U m s

theorem Dynamics.IsDynCoverOf.of_entourage_subset {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} {V : Set (X × X)} (U_V : U ⊆ V) {n : ℕ} {s : Set X} (h : Dynamics.IsDynCoverOf T F U n s) : Dynamics.IsDynCoverOf T F V n s

@[simp]

theorem Dynamics.isDynCoverOf_empty {X : Type u_1} {T : X → X} {U : Set (X × X)} {n : ℕ} {s : Set X} : Dynamics.IsDynCoverOf T ∅ U n s

theorem Dynamics.IsDynCoverOf.nonempty {X : Type u_1} {T : X → X} {F : Set X} (h : F.Nonempty) {U : Set (X × X)} {n : ℕ} {s : Set X} (h' : Dynamics.IsDynCoverOf T F U n s) : s.Nonempty

theorem Dynamics.isDynCoverOf_zero {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) {s : Set X} (h : s.Nonempty) : Dynamics.IsDynCoverOf T F U 0 s

theorem Dynamics.isDynCoverOf_univ {X : Type u_1} (T : X → X) (F : Set X) (n : ℕ) {s : Set X} (h : s.Nonempty) : Dynamics.IsDynCoverOf T F Set.univ n s

theorem Dynamics.IsDynCoverOf.nonempty_inter {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X} (h : Dynamics.IsDynCoverOf T F U n ↑s) : ∃ (t : Finset X), Dynamics.IsDynCoverOf T F U n ↑t ∧ t.card ≤ s.card ∧ ∀ x ∈ t, (UniformSpace.ball x (Dynamics.dynEntourage T U n) ∩ F).Nonempty

theorem Dynamics.IsDynCoverOf.iterate_le_pow {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) {m : ℕ} (n : ℕ) {s : Finset X} (h : Dynamics.IsDynCoverOf T F U m ↑s) : ∃ (t : Finset X), Dynamics.IsDynCoverOf T F (compRel U U) (m * n) ↑t ∧ t.card ≤ s.card ^ n

From a dynamical cover s with entourage U and time m, we construct covers with entourage U ○ U and any multiple m * n of m with controlled cardinality. This lemma is the first step in a submultiplicative-like property of coverMincard, with consequences such as explicit bounds for the topological entropy (coverEntropyInfEnt_le_card_div) and an equality between two notions of topological entropy (coverEntropyInf_eq_coverEntropySup_of_inv).

theorem Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F) (h : UniformContinuous T) {U : Set (X × X)} (U_uni : U ∈ uniformity X) (n : ℕ) : ∃ (s : Finset X), Dynamics.IsDynCoverOf T F U n ↑s

theorem Dynamics.exists_isDynCoverOf_of_isCompact_invariant {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F) (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ uniformity X) (n : ℕ) : ∃ (s : Finset X), Dynamics.IsDynCoverOf T F U n ↑s

Minimal cardinality of dynamical covers

noncomputable def Dynamics.coverMincard {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : ℕ∞

The smallest cardinality of a (U, n)-dynamical cover of F. Takes values in ℕ∞, and is infinite if and only if F admits no finite dynamical cover.

Equations

• Dynamics.coverMincard T F U n = ⨅ (s : Finset X), ⨅ (_ : Dynamics.IsDynCoverOf T F U n ↑s), ↑s.card

theorem Dynamics.coverMincard_le_card {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X} (h : Dynamics.IsDynCoverOf T F U n ↑s) : Dynamics.coverMincard T F U n ≤ ↑s.card

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

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

theorem Dynamics.coverMincard_finite_iff {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : Dynamics.coverMincard T F U n < ⊤ ↔ ∃ (s : Finset X), Dynamics.IsDynCoverOf T F U n ↑s ∧ ↑s.card = Dynamics.coverMincard T F U n

@[simp]

theorem Dynamics.coverMincard_empty {X : Type u_1} {T : X → X} {U : Set (X × X)} {n : ℕ} : Dynamics.coverMincard T ∅ U n = 0

theorem Dynamics.coverMincard_eq_zero_iff {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : Dynamics.coverMincard T F U n = 0 ↔ F = ∅

theorem Dynamics.one_le_coverMincard_iff {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : 1 ≤ Dynamics.coverMincard T F U n ↔ F.Nonempty

theorem Dynamics.coverMincard_zero {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) : Dynamics.coverMincard T F U 0 = 1

theorem Dynamics.coverMincard_univ {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) (n : ℕ) : Dynamics.coverMincard T F Set.univ n = 1

theorem Dynamics.coverMincard_mul_le_pow {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) (m : ℕ) (n : ℕ) : Dynamics.coverMincard T F (compRel U U) (m * n) ≤ Dynamics.coverMincard T F U m ^ n

theorem Dynamics.coverMincard_le_pow {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) {m : ℕ} (m_pos : 0 < m) (n : ℕ) : Dynamics.coverMincard T F (compRel U U) n ≤ Dynamics.coverMincard T F U m ^ (n / m + 1)

theorem Dynamics.coverMincard_finite_of_isCompact_uniformContinuous {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F) (h : UniformContinuous T) {U : Set (X × X)} (U_uni : U ∈ uniformity X) (n : ℕ) : Dynamics.coverMincard T F U n < ⊤

theorem Dynamics.coverMincard_finite_of_isCompact_invariant {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F) (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ uniformity X) (n : ℕ) : Dynamics.coverMincard T F U n < ⊤

theorem Dynamics.nonempty_inter_of_coverMincard {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X} (h : Dynamics.IsDynCoverOf T F U n ↑s) (h' : ↑s.card = Dynamics.coverMincard T F U n) (x : X) : x ∈ s → (F ∩ UniformSpace.ball x (Dynamics.dynEntourage T U n)).Nonempty

All dynamical balls of a minimal dynamical cover of F intersect F. This lemma is the key to relate Bowen-Dinaburg's definition of topological entropy with covers and their definition of topological entropy with nets.

theorem Dynamics.log_coverMincard_nonneg {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) (n : ℕ) : 0 ≤ (↑(Dynamics.coverMincard T F U n)).log

theorem Dynamics.log_coverMincard_iterate_le {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) (m : ℕ) {n : ℕ} (n_pos : 0 < n) : (↑(Dynamics.coverMincard T F (compRel U U) (m * n))).log / ↑n ≤ (↑(Dynamics.coverMincard T F U m)).log

theorem Dynamics.log_coverMincard_le_add {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) {m : ℕ} {n : ℕ} (m_pos : 0 < m) (n_pos : 0 < n) : (↑(Dynamics.coverMincard T F (compRel U U) n)).log / ↑n ≤ (↑(Dynamics.coverMincard T F U m)).log / ↑m + (↑(Dynamics.coverMincard T F U m)).log / ↑n

Cover entropy of entourages

noncomputable def Dynamics.coverEntropyEnt {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) : EReal

The entropy of an entourage U (Ent stands for "entourage"), defined as the exponential rate of growth of the size of the smallest (U, n)-refined cover of F. Takes values in the space of extended real numbers [-∞, +∞]. This first version uses a limsup, and is chosen as the default definition.

Equations

• Dynamics.coverEntropyEnt T F U = Filter.limsup (fun (n : ℕ) => (↑(Dynamics.coverMincard T F U n)).log / ↑n) Filter.atTop

noncomputable def Dynamics.coverEntropyInfEnt {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) : EReal

The entropy of an entourage U (Ent stands for "entourage"), defined as the exponential rate of growth of the size of the smallest (U, n)-refined cover of F. Takes values in the space of extended real numbers [-∞, +∞]. This second version uses a liminf, and is chosen as an alternative definition.

Equations

• Dynamics.coverEntropyInfEnt T F U = Filter.liminf (fun (n : ℕ) => (↑(Dynamics.coverMincard T F U n)).log / ↑n) Filter.atTop

theorem Dynamics.coverEntropyInfEnt_antitone {X : Type u_1} (T : X → X) (F : Set X) : Antitone fun (U : Set (X × X)) => Dynamics.coverEntropyInfEnt T F U

theorem Dynamics.coverEntropyEnt_antitone {X : Type u_1} (T : X → X) (F : Set X) : Antitone fun (U : Set (X × X)) => Dynamics.coverEntropyEnt T F U

theorem Dynamics.coverEntropyInfEnt_le_coverEntropyEnt {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) : Dynamics.coverEntropyInfEnt T F U ≤ Dynamics.coverEntropyEnt T F U

@[simp]

theorem Dynamics.coverEntropyEnt_empty {X : Type u_1} {T : X → X} {U : Set (X × X)} : Dynamics.coverEntropyEnt T ∅ U = ⊥

@[simp]

theorem Dynamics.coverEntropyInfEnt_empty {X : Type u_1} {T : X → X} {U : Set (X × X)} : Dynamics.coverEntropyInfEnt T ∅ U = ⊥

theorem Dynamics.coverEntropyInfEnt_nonneg {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) : 0 ≤ Dynamics.coverEntropyInfEnt T F U

theorem Dynamics.coverEntropyEnt_nonneg {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) : 0 ≤ Dynamics.coverEntropyEnt T F U

theorem Dynamics.coverEntropyEnt_univ {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) : Dynamics.coverEntropyEnt T F Set.univ = 0

theorem Dynamics.coverEntropyInfEnt_univ {X : Type u_1} (T : X → X) {F : Set X} (h : F.Nonempty) : Dynamics.coverEntropyInfEnt T F Set.univ = 0

theorem Dynamics.coverEntropyEnt_le_log_coverMincard_div {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} (n_pos : 0 < n) : Dynamics.coverEntropyEnt T F (compRel U U) ≤ (↑(Dynamics.coverMincard T F U n)).log / ↑n

theorem Dynamics.IsDynCoverOf.coverEntropyEnt_le_log_card_div {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} (n_pos : 0 < n) {s : Finset X} (h : Dynamics.IsDynCoverOf T F U n ↑s) : Dynamics.coverEntropyEnt T F (compRel U U) ≤ (↑s.card).log / ↑n

theorem Dynamics.coverEntropyEnt_le_coverEntropyInfEnt {X : Type u_1} {T : X → X} {F : Set X} (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) : Dynamics.coverEntropyEnt T F (compRel U U) ≤ Dynamics.coverEntropyInfEnt T F U

theorem Dynamics.coverEntropyEnt_finite_of_isCompact_invariant {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F) (F_inv : Set.MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ uniformity X) : Dynamics.coverEntropyEnt T F U < ⊤

Cover entropy

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

The entropy of T restricted to F, obtained by taking the supremum over entourages. Note that this supremum is approached by taking small entourages. This first version uses a limsup, and is chosen as the default definition for topological entropy.

Equations

• Dynamics.coverEntropy T F = ⨆ U ∈ uniformity X, Dynamics.coverEntropyEnt T F U

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

The entropy of T restricted to F, obtained by taking the supremum over entourages. Note that this supremum is approached by taking small entourages. This second version uses a liminf, and is chosen as an alternative definition for topological entropy.

Equations

• Dynamics.coverEntropyInf T F = ⨆ U ∈ uniformity X, Dynamics.coverEntropyInfEnt T F U

theorem Dynamics.coverEntropyInf_antitone {X : Type u_1} (T : X → X) (F : Set X) : Antitone fun (u : UniformSpace X) => Dynamics.coverEntropyInf T F

theorem Dynamics.coverEntropy_antitone {X : Type u_1} (T : X → X) (F : Set X) : Antitone fun (u : UniformSpace X) => Dynamics.coverEntropy T F

theorem Dynamics.coverEntropyEnt_le_coverEntropy {X : Type u_1} [UniformSpace X] (T : X → X) (F : Set X) {U : Set (X × X)} (h : U ∈ uniformity X) : Dynamics.coverEntropyEnt T F U ≤ Dynamics.coverEntropy T F

theorem Dynamics.coverEntropyInfEnt_le_coverEntropyInf {X : Type u_1} [UniformSpace X] (T : X → X) (F : Set X) {U : Set (X × X)} (h : U ∈ uniformity X) : Dynamics.coverEntropyInfEnt T F U ≤ Dynamics.coverEntropyInf T F

theorem Dynamics.coverEntropy_eq_iSup_basis {X : Type u_1} [UniformSpace X] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set (X × X)} (h : (uniformity X).HasBasis p s) (T : X → X) (F : Set X) : Dynamics.coverEntropy T F = ⨆ (i : ι), ⨆ (_ : p i), Dynamics.coverEntropyEnt T F (s i)

theorem Dynamics.coverEntropyInf_eq_iSup_basis {X : Type u_1} [UniformSpace X] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set (X × X)} (h : (uniformity X).HasBasis p s) (T : X → X) (F : Set X) : Dynamics.coverEntropyInf T F = ⨆ (i : ι), ⨆ (_ : p i), Dynamics.coverEntropyInfEnt T F (s i)

theorem Dynamics.coverEntropyInf_le_coverEntropy {X : Type u_1} [UniformSpace X] (T : X → X) (F : Set X) : Dynamics.coverEntropyInf T F ≤ Dynamics.coverEntropy T F

@[simp]

theorem Dynamics.coverEntropy_empty {X : Type u_1} [UniformSpace X] {T : X → X} : Dynamics.coverEntropy T ∅ = ⊥

@[simp]

theorem Dynamics.coverEntropyInf_empty {X : Type u_1} [UniformSpace X] {T : X → X} : Dynamics.coverEntropyInf T ∅ = ⊥

theorem Dynamics.coverEntropyInf_nonneg {X : Type u_1} [UniformSpace X] (T : X → X) {F : Set X} (h : F.Nonempty) : 0 ≤ Dynamics.coverEntropyInf T F

theorem Dynamics.coverEntropy_nonneg {X : Type u_1} [UniformSpace X] (T : X → X) {F : Set X} (h : F.Nonempty) : 0 ≤ Dynamics.coverEntropy T F

theorem Dynamics.coverEntropyInf_eq_coverEntropy {X : Type u_1} [UniformSpace X] (T : X → X) {F : Set X} (h : Set.MapsTo T F F) : Dynamics.coverEntropyInf T F = Dynamics.coverEntropy T F