English
The entropy of T restricted to F is defined as the supremum, over all entourages U, of the entropy contributed by that entourage, coverEntropyEntourage(T, F, U).
Русский
Энтропия T на F определяется как супремум по всем окрестностям U величины coverEntropyEntourage(T, F, U).
LaTeX
$$$\operatorname{coverEntropy}(T,F) = \sup_{U \in \mathcal{U}(X)} \operatorname{coverEntropyEntourage}(T,F,U)$$$
Lean4
/-- The entropy of `T` restricted to `F`, obtained by taking the supremum
of `coverEntropyEntourage` over entourages. Note that this supremum is approached by taking small
entourages. This first version uses a `limsup`, and is chosen as the default definition
for topological entropy. -/
noncomputable def coverEntropy [UniformSpace X] (T : X → X) (F : Set X) :=
⨆ U ∈ 𝓤 X, coverEntropyEntourage T F U
