Commit 2025-02-23 17:36 464fd974

feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) This file defines the exponential growth of a sequence u of ENNReals as the liminf/limsup of log (u n) / n. The immediate goal is to refactor files about Topological entropy (Dynamics.TopologicalEntropy.CoverEntropy, for instance): rewrite some definitions using expGrowths and replace most or all the analysis by applications of basic properties of expGrowth. At a later point, other notions may also be defined using this file: other notions of topological entropy, metric entropy, topological/metric pressure, Lyapunov exponents, large deviations...