feat(Analysis/Asymptotics): exponential growth of a sequence

[D-Thomine]

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...

---

[github-actions]

PR summary f4b03b36df

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Asymptotics.ExpGrowth (new file)	1665

---

Declarations diff

+ expGrowthInf
+ expGrowthInfTopHom
+ expGrowthInf_biInf
+ expGrowthInf_congr
+ expGrowthInf_const
+ expGrowthInf_eventually_monotone
+ expGrowthInf_iInf
+ expGrowthInf_inf
+ expGrowthInf_inv
+ expGrowthInf_le_expGrowthSup
+ expGrowthInf_le_iff
+ expGrowthInf_le_of_eventually_le
+ expGrowthInf_monotone
+ expGrowthInf_mul_le
+ expGrowthInf_mul_le'
+ expGrowthInf_of_eventually_ge
+ expGrowthInf_pow
+ expGrowthInf_top
+ expGrowthInf_zero
+ expGrowthSup
+ expGrowthSupBotHom
+ expGrowthSup_add
+ expGrowthSup_biSup
+ expGrowthSup_congr
+ expGrowthSup_const
+ expGrowthSup_eventually_monotone
+ expGrowthSup_iSup
+ expGrowthSup_inv
+ expGrowthSup_le_iff
+ expGrowthSup_le_of_eventually_le
+ expGrowthSup_monotone
+ expGrowthSup_mul_le
+ expGrowthSup_of_eventually_ge
+ expGrowthSup_pow
+ expGrowthSup_sum
+ expGrowthSup_sup
+ expGrowthSup_top
+ expGrowthSup_zero
+ le_expGrowthInf_add
+ le_expGrowthInf_iff
+ le_expGrowthInf_mul
+ le_expGrowthSup_iff
+ le_expGrowthSup_mul
+ le_expGrowthSup_mul'

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sgouezel]

Looks good, thanks!