English
Under a basis of the uniformity, the cover entropy equals the iSup over the basis elements of the corresponding net entropies, i.e., coverEntropyInf T F = ⨆ i (iSup over basis) netEntropyInfEntourage T F (s i).
Русский
При базисе униформности: coverEntropyInf T F = ⨆ i, netEntropyInfEntEnt Entourage T F (s i).
LaTeX
$$$\text{coverEntropyInf}(T,F)=\bigsqcup_{i}\,\text{netEntropyInfEnt Entourage}(T,F,(s_i))$$$
Lean4
/-- Bowen-Dinaburg's definition of topological entropy using nets is
`⨆ U ∈ 𝓤 X, netEntropyEntourage T F U`. This quantity is the same as the topological entropy using
covers, so there is no need to define a new notion of topological entropy. This version of the
theorem relates the `liminf` versions of topological entropy. -/
theorem coverEntropyInf_eq_iSup_netEntropyInfEntourage :
coverEntropyInf T F = ⨆ U ∈ 𝓤 X, netEntropyInfEntourage T F U :=
by
apply le_antisymm <;> refine iSup₂_le fun U U_uni ↦ ?_
· obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
apply (coverEntropyInfEntourage_antitone T F V_U).trans (le_iSup₂_of_le V V_uni _)
exact coverEntropyInfEntourage_le_netEntropyInfEntourage T F (refl_le_uniformity V_uni) V_symm
· apply (netEntropyInfEntourage_antitone T F (symmetrizeRel_subset_self U)).trans
apply (le_iSup₂ (symmetrizeRel U) (symmetrize_mem_uniformity U_uni)).trans'
exact netEntropyInfEntourage_le_coverEntropyInfEntourage T F (symmetric_symmetrizeRel U)
