Topological entropy via nets

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

The major design decisions are the same as in Mathlib.Dynamics.TopologicalEntropy.CoverEntropy, and are explained in detail there: use of uniform spaces, definition of the topological entropy of a subset, and values taken in EReal.

Given a map T : X → X and a subset F ⊆ X, the topological entropy is loosely defined using nets as the exponential growth (in n) of the number of distinguishable orbits of length n starting from F. More precisely, given an entourage U, two orbits of length n can be distinguished if there exists some index k < n such that T^[k] x and T^[k] y are far enough (i.e. (T^[k] x, T^[k] y) is not in U). The maximal number of distinguishable orbits of length n is netMaxcard T F U n, and its exponential growth netEntropyEntourage T F U. This quantity increases when U decreases, and a definition of the topological entropy is ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U.

The definition of topological entropy using nets coincides with the definition using covers. Instead of defining a new notion of topological entropy, we prove that coverEntropy coincides with ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U.

Main definitions

• IsDynNetIn: property that dynamical balls centered on a subset s of F are disjoint.
• netMaxcard: maximal cardinality of a dynamical net. Takes values in ℕ∞.
• netEntropyInfEntourage/netEntropyEntourage: exponential growth of netMaxcard. The former is defined with a liminf, the latter with a limsup. Take values in EReal.

Implementation notes

As when using covers, there are two competing definitions netEntropyInfEntourage and netEntropyEntourage in this file: one uses a liminf, the other a limsup. When using covers, we chose the limsup definition as the default.

Main results

• coverEntropy_eq_iSup_netEntropyEntourage: equality between the notions of topological entropy defined with covers and with nets. Has a variant for coverEntropyInf.

Tags

net, entropy

TODO

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

Dynamical nets

def Dynamics.IsDynNetIn {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 of F is a (U, n)-dynamical net of F if no two orbits of length n of points in s shadow each other.

Equations

• Dynamics.IsDynNetIn T F U n s = (s ⊆ F ∧ s.PairwiseDisjoint fun (x : X) => UniformSpace.ball x (Dynamics.dynEntourage T U n))

theorem Dynamics.IsDynNetIn.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.IsDynNetIn T F U m s) : Dynamics.IsDynNetIn T F U n s

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

theorem Dynamics.isDynNetIn_empty {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} : Dynamics.IsDynNetIn T F U n ∅

theorem Dynamics.isDynNetIn_singleton {X : Type u_1} (T : X → X) {F : Set X} (U : Set (X × X)) (n : ℕ) {x : X} (h : x ∈ F) : Dynamics.IsDynNetIn T F U n {x}

theorem Dynamics.IsDynNetIn.card_le_card_of_isDynCoverOf {X : Type u_1} {T : X → X} {F : Set X} {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} {s t : Finset X} (hs : Dynamics.IsDynNetIn T F U n ↑s) (ht : Dynamics.IsDynCoverOf T F U n ↑t) : s.card ≤ t.card

Given an entourage U and a time n, a dynamical net has a smaller cardinality than a dynamical cover. This lemma is the first of two key results to compare two versions of topological entropy: with cover and with nets, the second being coverMincard_le_netMaxcard.

Maximal cardinality of dynamical nets

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

The largest cardinality of a (U, n)-dynamical net of F. Takes values in ℕ∞, and is infinite if and only if F admits nets of arbitrarily large size.

Equations

• Dynamics.netMaxcard T F U n = ⨆ (s : Finset X), ⨆ (_ : Dynamics.IsDynNetIn T F U n ↑s), ↑s.card

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

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

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

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

@[simp]

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

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

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

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

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

theorem Dynamics.netMaxcard_infinite_iff {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : Dynamics.netMaxcard T F U n = ⊤ ↔ ∀ (k : ℕ), ∃ (s : Finset X), Dynamics.IsDynNetIn T F U n ↑s ∧ k ≤ s.card

theorem Dynamics.netMaxcard_le_coverMincard {X : Type u_1} (T : X → X) (F : Set X) {U : Set (X × X)} (U_symm : SymmetricRel U) (n : ℕ) : Dynamics.netMaxcard T F U n ≤ Dynamics.coverMincard T F U n

theorem Dynamics.coverMincard_le_netMaxcard {X : Type u_1} (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U) (U_symm : SymmetricRel U) (n : ℕ) : Dynamics.coverMincard T F (compRel U U) n ≤ Dynamics.netMaxcard T F U n

Given an entourage U and a time n, a minimal dynamical cover by U ○ U has a smaller cardinality than a maximal dynamical net by U. This lemma is the second of two key results to compare two versions topological entropy: with cover and with nets.

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

Net entropy of entourages

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

The entropy of an entourage U, defined as the exponential rate of growth of the size of the largest (U, n)-dynamical net of F. Takes values in the space of extended real numbers [-∞,+∞]. This version uses a limsup, and is chosen as the default definition.

Equations

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

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

The entropy of an entourage U, defined as the exponential rate of growth of the size of the largest (U, n)-dynamical net of F. Takes values in the space of extended real numbers [-∞,+∞]. This version uses a liminf, and is an alternative definition.

Equations

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

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

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

theorem Dynamics.netEntropyInfEntourage_le_netEntropyEntourage {X : Type u_1} (T : X → X) (F : Set X) (U : Set (X × X)) : Dynamics.netEntropyInfEntourage T F U ≤ Dynamics.netEntropyEntourage T F U

@[simp]

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

@[simp]

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

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

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

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

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

theorem Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage {X : Type u_1} (T : X → X) (F : Set X) {U : Set (X × X)} (U_symm : SymmetricRel U) : Dynamics.netEntropyInfEntourage T F U ≤ Dynamics.coverEntropyInfEntourage T F U

theorem Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage {X : Type u_1} (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U) (U_symm : SymmetricRel U) : Dynamics.coverEntropyInfEntourage T F (compRel U U) ≤ Dynamics.netEntropyInfEntourage T F U

theorem Dynamics.netEntropyEntourage_le_coverEntropyEntourage {X : Type u_1} (T : X → X) (F : Set X) {U : Set (X × X)} (U_symm : SymmetricRel U) : Dynamics.netEntropyEntourage T F U ≤ Dynamics.coverEntropyEntourage T F U

theorem Dynamics.coverEntropyEntourage_le_netEntropyEntourage {X : Type u_1} (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U) (U_symm : SymmetricRel U) : Dynamics.coverEntropyEntourage T F (compRel U U) ≤ Dynamics.netEntropyEntourage T F U

Relationship with entropy via covers

theorem Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage {X : Type u_1} [UniformSpace X] (T : X → X) (F : Set X) : Dynamics.coverEntropyInf T F = ⨆ U ∈ uniformity X, Dynamics.netEntropyInfEntourage T F U

Bowen-Dinaburg's definition of topological entropy using nets is ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U. This quantity is the same as the topological entropy using covers, so there is no need to define a new notion of topological entropy. This version of the theorem relates the liminf versions of topological entropy.

theorem Dynamics.coverEntropy_eq_iSup_netEntropyEntourage {X : Type u_1} [UniformSpace X] (T : X → X) (F : Set X) : Dynamics.coverEntropy T F = ⨆ U ∈ uniformity X, Dynamics.netEntropyEntourage T F U

Bowen-Dinaburg's definition of topological entropy using nets is ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U. This quantity is the same as the topological entropy using covers, so there is no need to define a new notion of topological entropy. This version of the theorem relates the limsup versions of topological entropy.

theorem Dynamics.coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage {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.netEntropyInfEntourage T F (s i)

theorem Dynamics.coverEntropy_eq_iSup_basis_netEntropyEntourage {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.netEntropyEntourage T F (s i)

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

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