Include Topological entropy

[D-Thomine]

As mentioned in Zulip chat, I've got an ongoing project on formalizing Bowen-Dinaburg's version of topological entropy. I would like to add it to your project : there are some design decisions I would like a feedback on (including nomenclature), and areas which are surely inefficient. I think working together may also help get clean files on Mathlib and finding reviewers for them.

As of now, this project consists of 12 files of varying size :

• Invariant subsets (300l.) : my own version of statements about invariant subsets. Includes things about closed/compact subsets, but I actually only use the first two or three lemmas in the remainder of the project, so I can easily replace it by somebody else's version.
• Misc (400l.) : A hodgepodge of various lemma I should add to mathlib (but you always have new ones to add to this file...).
• ENNReal logarithm (280l.) : properties of the log from [0,infty] to [-infty, infty]. Finished, a review would be nice.
• EReal division (150l.) : division on [-infty, infty] and its properties. Finished, a review would be nice.
• EReal multiplication continuity (130l.) : continuity of the multiplication on [-infty, infty]. Finished, a review would be nice.
• Dynamical uniformity (180l.) : Dynamical balls (in the vocabulary of uniform spaces). Good to publish, but frequently modified.
• Dynamical cover (700l.) : Bowen-Dinaburg's definition(s) of the entropy with covers. Finished, a review would be nice.
• Dynamical net (560l.) : Bowen-Dinaburg's definition(s) of the entropy with nets. Finished, a review would be nice.

Plus 4 files about the entropy of various systems (subsets, unions, products, semi-conjugacies) which I've decided to keep separated. 2 are finished, and 2 are almost finished (but I have serious issues working with limits in Lean, so any help is appreciated -- I can prove what I want, but this tends to be very inefficient).

If you are interested to this work, I'll add a documentation page to clarify the structure and dependence of these files, as well as the design decisions I made.

Would you agree to home this project on BET, or would you prefer I find somewhere else ?

[oliver-butterley]

You have done a huge amount! Great! Personally I'm very happy to be part of this and enthusiastic to spend time on this.

@mseri?

We should also figure out a systematic way to queue all the results which are essentially ready for final polishing and moving to mathlib.

[mseri]

Sounds very good and interesting to me, amazing job. It think keeping it in one place while we start preparing and moving it to mathlib is a good idea also to avoid duplication of efforts.

In the meantime, we should really brainstorm what could be a good way to structure the work and the planning. And also how to remain faithful to our objective of keeping the project a good playground to learn lean/mathlib along the way.

[mseri]

This was merged in https://github.com/mseri/BET/pull/44 We can now open separate issues on the various TODOs when we are ready to address them