Port TopologicalEntropy to Mathlib

[pitmonticone]

• https://github.com/leanprover-community/mathlib4/pull/14018
• https://github.com/leanprover-community/mathlib4/pull/14019
• https://github.com/leanprover-community/mathlib4/pull/14066
• https://github.com/leanprover-community/mathlib4/pull/14096
• https://github.com/leanprover-community/mathlib4/pull/14102
• https://github.com/leanprover-community/mathlib4/pull/14125
• https://github.com/leanprover-community/mathlib4/pull/14128
• https://github.com/leanprover-community/mathlib4/pull/14169
• https://github.com/leanprover-community/mathlib4/pull/14107
• https://github.com/leanprover-community/mathlib4/pull/14224
• https://github.com/leanprover-community/mathlib4/pull/14329
• https://github.com/leanprover-community/mathlib4/pull/14564

[mseri]

Part of https://github.com/mseri/BET/issues/55