English
The entropy of an entourage U, denoting the exponential growth rate of the size of the largest (U, n)-dynamical net of F, is defined by netEntropyEntourage(T,F,U) = expGrowthSup(n ↦ netMaxcard T F U n). It takes values in the extended real numbers.
Русский
Энтропия окрестности U задаётся как экспоненциальная скорость роста величины наибольшей (U, n)-динамической сети F, то есть netEntropyEntourage(T,F,U) = expGrowthSup(n ↦ netMaxcard T F U n). Значение лежит в расширенных вещественных числах.
LaTeX
$$$\operatorname{netEntropyEntourage}(T,F,U)=\operatorname{expGrowthSup}(n\mapsto \operatorname{netMaxcard}(T,F,U,n))$$$
Lean4
/-- The entropy of an entourage `U`, defined as the exponential rate of growth of the size of the
largest `(U, n)`-dynamical net of `F`. Takes values in the space of extended real numbers
`[-∞,+∞]`. This version uses a `limsup`, and is chosen as the default definition. -/
noncomputable def netEntropyEntourage (T : X → X) (F : Set X) (U : Set (X × X)) :=
expGrowthSup fun n : ℕ ↦ netMaxcard T F U n
