Commit 2024-08-12 19:34 9e8eaf98

View on Github →

feat(Dynamics): add TopologicalEntropy.DynamicalUniformity (#14938) First PR in a sequence to implement the notion of topological entropy for maps using Bowen-Dinaburg's formalism. This file describes a notion of dynamical uniformities, which generalizes dynamical balls in metric spaces.

Dynamical uniformities
Topological entropy via covers
Topological entropy via nets
Behaviour for subsets
Behaviour under morphisms
Behaviour under union
Behaviour under products
Full shift This file is pretty short; the next ones are more involved. Paging @pitmonticone @sgouezel

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

added def Dynamics.dynEntourage

added theorem Dynamics.dynEntourage_antitone

added theorem Dynamics.dynEntourage_comp_subset

added theorem Dynamics.dynEntourage_eq_inter_Ico

added theorem Dynamics.dynEntourage_mem_uniformity

added theorem Dynamics.dynEntourage_monotone

added theorem Dynamics.dynEntourage_one

added theorem Dynamics.dynEntourage_univ

added theorem Dynamics.dynEntourage_zero

added theorem Dynamics.idRel_subset_dynEntourage

added theorem Dynamics.mem_ball_dynEntourage

added theorem Dynamics.mem_ball_dynEntourage_comp

added theorem Dynamics.mem_dynEntourage

added theorem Function.Semiconj.preimage_dynEntourage

added theorem SymmetricRel.dynEntourage

added theorem isOpen.dynEntourage