Topological Entropy: required updates for mathlib-ization

[mseri]

To-Do List

• Port IsInvariant and inv_def' from InvariantSubset.lean (needs to be harmonized/unified with IsInvariant under Flow in mathlib)
• Move results on invariance and orbits from Topologica.lean/Minimal.lean into InvariantSubset.lean
• Port univ_is_inv and empty_is_inv' from InvariantSubset.lean
• Port the whole ENNRealLog.lean
• Port the whole ERealMulCont.lean incorporating the auxiliary lemmas into the main theorem proof or making them private lemmas + golfing + PR to to the file on multiplication on EReal.
• Port the whole ERealDiv.lean
• Port the whole Inv.lean
• Port Misc.lean to WithBot, PR to logical files. Up to open Filter: golf check + put on the file EREals. After open Filter put on the file EReal.Filter (+ directory for EREal?)
• Port the whole DynamicalUniformity.lean: necessary cleanup.
• Port the whole DynamicalDover.lean: choose a good name for cover entropy
• Port the whole Subset.lean: necessary cleanup.
• Port the whole Morphism.lean: rename semiconjugacy
• Port the whole EReal.lean: necessary cleanup
• Port the whole Shift.lean: almost
• Union.lean is unfinished and painful (ideally bypassing limits)
• Product.lean is unfinished but close to completion

Please create a separate issue for each for these if you are working on them, and link (or let us link) the issue number next to the corresponding item.

[mseri]

Thanks @pitmonticone for the carefully crafted list and @D-Thomine for the detailed walkthrough

[D-Thomine]

Still working on porting Misc.lean.

Done: moving prod_ite from Dynamics to Functions.

Open: PR#14564 to get characterizations of limsup/liminf in the main Order.LiminfLimsup file. Cannot compile because the file is too large (linter flag).

Soon to be opened: adding a few things on Topology.UniformSpace.Basic about products. This should finish the current content of Misc.lean. The branch is D-Thomine/uniformity_prod

Paging @pitmonticone

[pitmonticone]

Hi @D-Thomine, great job!

I'll try to refactor in order to "solve" that linter issue later today, but it's highly likely to be acceptable simply adding a style-exception.

[pitmonticone]

See the relevant Zulip topic https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Porting.20TopologicalEntropy.20into.20Mathlib

[pitmonticone]

Solved here