Commit 2025-04-18 09:15 c7e8bc78
View on Github →refactor(Dynamics/TopologicalEntropy): use expGrowth (#23554)
The notions of coverEntropyEntourage, coverEntropyInfEntourage, netEntropyEntourage and netEntropyInfEntourage are now defined using expGrowth. Some technical intermediate lemmas are no longer needed and are removed.
Some minor golfing around those three files.