English
The second variant of entropy of an entourage U is given by the infimum-based growth: coverEntropyInfEntourage(T,F,U) = expGrowthInf(n ↦ coverMincard T F U n).
Русский
Вторая версия энтропии окружения U задаётся как экспоненциальный рост с помощью inf: coverEntropyInfEntourage(T,F,U) = expGrowthInf(n ↦ coverMincard T F U n).
LaTeX
$$$\mathrm{coverEntropyInfEntourage}(T,F,U) = \mathrm{expGrowthInf}\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 second version uses a `liminf`, and is chosen as an alternative definition. -/
noncomputable def coverEntropyInfEntourage (T : X → X) (F : Set X) (U : Set (X × X)) :=
expGrowthInf fun n : ℕ ↦ coverMincard T F U n
