English
The entropy of an entourage via liminf is defined by netEntropyInfEntourage(T,F,U) = expGrowthInf(n ↦ netMaxcard T F U n).
Русский
Энтропия окрестности через лиминф или предельное нижнее значение задаётся как netEntropyInfEntourage(T,F,U) = expGrowthInf(n ↦ netMaxcard T F U n).
LaTeX
$$$\operatorname{netEntropyInfEntourage}(T,F,U)=\operatorname{expGrowthInf}(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 `liminf`, and is an alternative definition. -/
noncomputable def netEntropyInfEntourage (T : X → X) (F : Set X) (U : Set (X × X)) :=
expGrowthInf fun n : ℕ ↦ netMaxcard T F U n
