mseri/bet

Project for "Machine-Checked Mathematics" at the Lorentz Center

bet's Issues

Fix file headers with the license

/-
Copyright (c) 2023 "one of us". All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Butterley, Guillaume Dubach, Marco Lenci, Sébastien Gouëzel, Marcello Seri, ...
-/

Ensure that whatever other person contributed is in the list

Include Topological entropy

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 ?

Minimal.lean to be polished and harmonized with mathlib

See https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Dynamics/Minimal.lean

Our minimal sets need to be extended to action and topological spaces

Split topological.lean into its functional components

The file contains nonwandering sets, recurrent sets and minimal sets.
They should be split into meaningful functional bits. E.g.

topological/{nonWandering.lean, recurrent.lean, minimalSet.lean}

and polished so that they can be contributed back to Mathlib.Dynamics: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Dynamics/

Complete the final part of birkhoff's ergodic theorem

Add documentation to Birkhoff.lean

As per title

Merge the minimal set existence results into `minimal.lean`

Merge relevant changes from WIP to the main branch

Make Topological.lean really topological

Blocking #24, see the discussion in that issue

Topological Entropy: required updates for `mathlib`-ization

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 + golfing + PR to to the file on multiplication on EReal.
• Port the whole ERealDiv.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.

Update the workflow to take advantage of `lean-action`

The workflow which builds on push and PR can be updated to take advantage of https://github.com/leanprover/lean-action.

lean-action is currently in development so it will be useful also to test it in a real situation.

Update lakefile.lean to toml version

Swap from lakefile.lean to lakefile.toml (zulip iscussion).

Update the workflow to take advantage of `lean-update`

Workflow can be updated to use https://github.com/oliver-butterley/lean-update

But some minor modifications should be made to the action in advance of this.