Topological entropy of the image of a set under a semiconjugacy

Consider two dynamical systems (X, S) and (Y, T) together with a semiconjugacy φ:

X ---S--> X
|         |
φ         φ
|         |
v         v
Y ---T--> Y

We relate the topological entropy of a subset F ⊆ X with the topological entropy of its image φ '' F ⊆ Y.

The best-known theorem is that, if all maps are uniformly continuous, then coverEntropy T (φ '' F) ≤ coverEntropy S F. This is theorem coverEntropy_image_le_of_uniformContinuous herein. We actually prove the much more general statement that coverEntropy T (φ '' F) = coverEntropy S F if X is endowed with the pullback by φ of the uniform structure of Y.

This more general statement has another direct consequence: if F is S-invariant, then the topological entropy of the restriction of S to F is exactly coverEntropy S F. This corollary is essential: in most references, the entropy of an invariant subset (or subsystem) F is defined as the entropy of the restriction to F of the system. We chose instead to give a direct definition of the topological entropy of a subset, so as to avoid working with subtypes. Theorem coverEntropy_restrict shows that this choice is coherent with the literature.

Implementation notes

We use only the definition of the topological entropy using covers; the simplest version of IsDynCoverOf.image for nets fails.

Main results

• coverEntropy_image_of_comap/coverEntropyInf_image_of_comap: the entropy of φ '' F equals the entropy of F if X is endowed with the pullback by φ of the uniform structure of Y.
• coverEntropy_image_le_of_uniformContinuous/coverEntropyInf_image_le_of_uniformContinuous: the entropy of φ '' F is lower than the entropy of F if φ is uniformly continuous.
• coverEntropy_restrict: the entropy of the restriction of S to an invariant set F is coverEntropy S F.

Tags

entropy, semiconjugacy

theorem Dynamics.IsDynCoverOf.image {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) {F : Set X} {V : Set (Y × Y)} {n : ℕ} {s : Set X} (h' : Dynamics.IsDynCoverOf S F (Prod.map φ φ ⁻¹' V) n s) : Dynamics.IsDynCoverOf T (φ '' F) V n (φ '' s)

theorem Dynamics.IsDynCoverOf.preimage {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) {F : Set X} {V : Set (Y × Y)} (V_symm : SymmetricRel V) {n : ℕ} {t : Finset Y} (h' : Dynamics.IsDynCoverOf T (φ '' F) V n ↑t) : ∃ (s : Finset X), Dynamics.IsDynCoverOf S F (Prod.map φ φ ⁻¹' compRel V V) n ↑s ∧ s.card ≤ t.card

theorem Dynamics.le_coverMincard_image {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) {V : Set (Y × Y)} (V_symm : SymmetricRel V) (n : ℕ) : Dynamics.coverMincard S F (Prod.map φ φ ⁻¹' compRel V V) n ≤ Dynamics.coverMincard T (φ '' F) V n

theorem Dynamics.coverMincard_image_le {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) (n : ℕ) : Dynamics.coverMincard T (φ '' F) V n ≤ Dynamics.coverMincard S F (Prod.map φ φ ⁻¹' V) n

theorem Dynamics.le_coverEntropyEntourage_image {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) {V : Set (Y × Y)} (V_symm : SymmetricRel V) : Dynamics.coverEntropyEntourage S F (Prod.map φ φ ⁻¹' compRel V V) ≤ Dynamics.coverEntropyEntourage T (φ '' F) V

theorem Dynamics.le_coverEntropyInfEntourage_image {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) {V : Set (Y × Y)} (V_symm : SymmetricRel V) : Dynamics.coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' compRel V V) ≤ Dynamics.coverEntropyInfEntourage T (φ '' F) V

theorem Dynamics.coverEntropyEntourage_image_le {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) : Dynamics.coverEntropyEntourage T (φ '' F) V ≤ Dynamics.coverEntropyEntourage S F (Prod.map φ φ ⁻¹' V)

theorem Dynamics.coverEntropyInfEntourage_image_le {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) : Dynamics.coverEntropyInfEntourage T (φ '' F) V ≤ Dynamics.coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V)

theorem Dynamics.coverEntropy_image_of_comap {X : Type u_1} {Y : Type u_2} (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) : Dynamics.coverEntropy T (φ '' F) = Dynamics.coverEntropy S F

The entropy of φ '' F equals the entropy of F if X is endowed with the pullback by φ of the uniform structure of Y.

theorem Dynamics.coverEntropyInf_image_of_comap {X : Type u_1} {Y : Type u_2} (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (F : Set X) : Dynamics.coverEntropyInf T (φ '' F) = Dynamics.coverEntropyInf S F

The entropy of φ '' F equals the entropy of F if X is endowed with the pullback by φ of the uniform structure of Y. This version uses a liminf.

theorem Dynamics.coverEntropy_restrict_subset {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} {G : Set X} (hF : F ⊆ G) (hG : Set.MapsTo T G G) : Dynamics.coverEntropy (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropy T F

theorem Dynamics.coverEntropyInf_restrict_subset {X : Type u_1} [UniformSpace X] {T : X → X} {F : Set X} {G : Set X} (hF : F ⊆ G) (hG : Set.MapsTo T G G) : Dynamics.coverEntropyInf (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropyInf T F

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

The entropy of the restriction of T to an invariant set F is coverEntropy S F. This theorem justifies our definition of coverEntropy T F.

theorem Dynamics.coverEntropy_image_le_of_uniformContinuous {X : Type u_1} {Y : Type u_2} [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) : Dynamics.coverEntropy T (φ '' F) ≤ Dynamics.coverEntropy S F

The entropy of φ '' F is lower than entropy of F if φ is uniformly continuous.

theorem Dynamics.coverEntropyInf_image_le_of_uniformContinuous {X : Type u_1} {Y : Type u_2} [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) : Dynamics.coverEntropyInf T (φ '' F) ≤ Dynamics.coverEntropyInf S F

The entropy of φ '' F is lower than entropy of F if φ is uniformly continuous. This version uses a liminf.

theorem Dynamics.coverEntropy_image_le_of_uniformContinuousOn_invariant {X : Type u_1} {Y : Type u_2} [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) {F : Set X} {G : Set X} (h' : UniformContinuousOn φ G) (hF : F ⊆ G) (hG : Set.MapsTo S G G) : Dynamics.coverEntropy T (φ '' F) ≤ Dynamics.coverEntropy S F

theorem Dynamics.coverEntropyInf_image_le_of_uniformContinuousOn_invariant {X : Type u_1} {Y : Type u_2} [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y} (h : Function.Semiconj φ S T) {F : Set X} {G : Set X} (h' : UniformContinuousOn φ G) (hF : F ⊆ G) (hG : Set.MapsTo S G G) : Dynamics.coverEntropyInf T (φ '' F) ≤ Dynamics.coverEntropyInf S F