Commit 2024-10-11 18:32 ae22b2a2

View on Github →

feat(Dynamics.TopologicalEntropy.Semiconj): topological entropy and semiconjugacies (#17387) Fourth PR in a sequence to implement the notion of topological entropy for maps using Bowen-Dinaburg's formalism. This file deals with the entropy of two systems related by a semiconjugacy.

Dynamical uniformities
Topological entropy via covers
Topological entropy via nets
Behaviour under semiconjugacy
Behaviour for subsets and unions
Behaviour under products
Full shift There is only one new file, Dynamics.TopologicalEntropy.Semiconj, which is quite short (200 lines including the documentation), and no other modification. I must say I am quite pleased by coverEntropy_image. Paging @pitmonticone @sgouezel

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean

added theorem Dynamics.IsDynCoverOf.image

added theorem Dynamics.IsDynCoverOf.preimage

added theorem Dynamics.coverEntropyEntourage_image_le

added theorem Dynamics.coverEntropyInfEntourage_image_le

added theorem Dynamics.coverEntropyInf_image_le_of_uniformContinuous

added theorem Dynamics.coverEntropyInf_image_le_of_uniformContinuousOn_invariant

added theorem Dynamics.coverEntropyInf_image_of_comap

added theorem Dynamics.coverEntropyInf_restrict_subset

added theorem Dynamics.coverEntropy_image_le_of_uniformContinuous

added theorem Dynamics.coverEntropy_image_le_of_uniformContinuousOn_invariant

added theorem Dynamics.coverEntropy_image_of_comap

added theorem Dynamics.coverEntropy_restrict

added theorem Dynamics.coverEntropy_restrict_subset

added theorem Dynamics.coverMincard_image_le

added theorem Dynamics.le_coverEntropyEntourage_image

added theorem Dynamics.le_coverEntropyInfEntourage_image

added theorem Dynamics.le_coverMincard_image