feat(Dynamics.TopologicalEntropy): add definition of topological entr…

…opy by nets (#16162) Third PR in a sequence to implement the notion of topological entropy for maps using Bowen-Dinaburg's formalism. This file introduces a definition of topological entropy using nets. - [x] Dynamical uniformities - [x] Topological entropy via covers - [x] Topological entropy via nets - [ ] Behaviour under semiconjugacy - [ ] Behaviour for subsets and unions - [ ] Behaviour under products - [ ] Full shift The main file is `Dynamics.TopologicalEntropy.NetEntropy`. It is slightly shorter and less technical than the previous one. There are also a few modifications to `Dynamics.TopologicalEntropy.CoverEntropy` (some golf, and renamed a lemma to enable dot notation -- which is quite convenient here). Paging @pitmonticone @sgouezel Co-authored-by: Pietro Monticone <[email protected]>
leanprover-community · Sep 25, 2024 · 76338db · 76338db
1 parent 2ab87b4
commit 76338db
Show file tree

Hide file tree

Showing 3 changed files with 515 additions and 103 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2642,6 +2642,7 @@ import Mathlib.Dynamics.OmegaLimit
 import Mathlib.Dynamics.PeriodicPts
 import Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
 import Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
+import Mathlib.Dynamics.TopologicalEntropy.NetEntropy
 import Mathlib.FieldTheory.AbelRuffini
 import Mathlib.FieldTheory.AbsoluteGaloisGroup
 import Mathlib.FieldTheory.Adjoin