English
The entropy of an entourage U is defined as the exponential growth of the minimal cover numbers: coverEntropyEntourage(T,F,U) = expGrowthSup(n ↦ coverMincard T F U n).
Русский
Энтропия окружения U определяется как показатель экспоненциального роста минимальных чисел покрытий: coverEntropyEntourage(T,F,U) = expGrowthSup(n ↦ coverMincard T F U n).
LaTeX
$$$\mathrm{coverEntropyEntourage}(T,F,U) = \mathrm{expGrowthSup}\big(n \mapsto \mathrm{coverMincard}(T,F,U,n)\big)$$$
Lean4
/-- The entropy of an entourage `U`, defined as the exponential rate of growth of the size
of the smallest `(U, n)`-refined cover of `F`. Takes values in the space of extended real numbers
`[-∞, +∞]`. This first version uses a `limsup`, and is chosen as the default definition. -/
noncomputable def coverEntropyEntourage (T : X → X) (F : Set X) (U : Set (X × X)) :=
expGrowthSup fun n : ℕ ↦ coverMincard T F U n
