English
Let X be a uniform space, T: X → X, F ⊆ X a compact invariant set (i.e., F is compact and T(F) ⊆ F). For every entourage U in the uniformity of X, the entropy associated to this entourage, coverEntropyEntourage(T, F, U), is finite.
Русский
Пусть X — униформное пространство, T: X → X, F ⊆ X — компактное инвариантное множество (то есть F компактно и T(F) ⊆ F). Для любой окрестности U в униформной структуре X энтропия, связанная с этой окрестностью, coverEntropyEntourage(T, F, U), конечно.
LaTeX
$$$\forall U \in \mathcal{U}(X): \operatorname{coverEntropyEntourage}(T,F,U) < \infty$$$
Lean4
theorem coverEntropyEntourage_finite_of_isCompact_invariant [UniformSpace X] {T : X → X} {F : Set X}
(F_comp : IsCompact F) (F_inv : MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) :
coverEntropyEntourage T F U < ⊤ :=
by
obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv V_uni 1
apply (coverEntropyEntourage_antitone T F V_U).trans_lt
apply (s_cover.coverEntropyEntourage_le_log_card_div F_inv V_symm one_ne_zero).trans_lt
rw [Nat.cast_one, div_one, log_lt_top_iff, ← ENat.toENNReal_top]
exact_mod_cast (ENat.coe_ne_top (Finset.card s)).lt_top
