Porting TopologicalEntropy into Mathlib

Stream: mathlib4

[Pietro Monticone]

This topic is dedicated to the porting of TopologicalEntropy from this repository to Mathlib in collaboration with @Damien Thomine.

Draft PRs:

• None

Open PRs:

• #14107

Merged PRs:

• #14018
• #14019
• #14066
• #14096
• #14102
• #14125
• #14224
• #14169
• #14128
• #14329

[Sébastien Gouëzel]

Thanks for the PRs! A general comment from looking at the PRs: for each statements, try to see if it is in the proper generality, and if not then reformulate things in the right generality. Trying to do things right is always better than trying to them quickly (because in the end it will be quicker to do them right :-)

[Pietro Monticone]

Thank you @Sébastien Gouëzel for your reviews. Super helpful!

[Pietro Monticone]

In #14018 we have ported the extended nonnegative real logarithm adding the file ENNReal.lean into Analysis/SpecialFunctions/Log.

Now @Lorenzo Luccioli and I are working to port the extended exponential from the TLB (@Rémy Degenne) project into Mathlib.

How should we arrange everything? Should we put log and exp together in a single file?

Consider that we have results involving both functions such as:

lemma log_exp (x : EReal) : log (exp x) = x.

[Kim Morrison]

Separate files are great! Almost certainly one of these files needs to be downstream of the other, so put the lemmas about both functions in the naturally downstream file, or even in something like SpecialFunctions/Exp/Log!

[Pietro Monticone]

Opened #14125

[Pietro Monticone]

In #14125, I get this error:

::ERR file=Mathlib/Data/Real/EReal.lean,line=1,code=ERR_NUM_LIN::Mathlib/Data/Real/EReal.lean:1 ERR_NUM_LIN: file contains 1528 lines (at most 1700 allowed), try to split it up

What's the optimal way to proceed?

[Pietro Monticone]

Would it be enough to add

Mathlib/Data/Real/EReal.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1528 lines, try to split it up

to the style-exception.txt file?

[Kim Morrison]

Yes, that's right. Sorry about this. This linter is well intentioned but a nightmare to users.

[Pietro Monticone]

Kim Morrison said:

Yes, that's right. Sorry about this. This linter is well intentioned but a nightmare to users.

Ok, thanks. Done.

[Dean Young]

Question: is EReal the total space of Eℝ ⭢ Bℝ, in which π₁(Bℝ) is ℝ as a discrete abelian group?

[Pietro Monticone]

Opened #14128

[Pietro Monticone]

Opened #14169

[Pietro Monticone]

Opened #14194.

[Pietro Monticone]

This PR (#14194) adds prod_map_iterate.

I don't know what is supposed to be the optimal location for this theorem.

#find_home! prod_map_iterate suggested this file, but I am not sure where exactly it should be put within that file.

[Pietro Monticone]

Opened #14224 adding inverse and division of extended reals.

[Pietro Monticone]

Opened #14107

[Pietro Monticone]

Opened #14329

[Pietro Monticone]

Opened #14564.

We encountered another ERR_NUM_LIN since the file contains more than 1700 lines.

Can we just add the associated style exception, @Kim Morrison ?

[Michael Rothgang]

Pietro Monticone said:

Kim Morrison said:

Yes, that's right. Sorry about this. This linter is well intentioned but a nightmare to users.

Ok, thanks. Done.

For anybody coming here later: #14012 has improved the error message of the linter (I agree the previous formatting was terrible!, it was meant for github annotations and not for humans); #14273 adds a simple command for just adding the style exceptions. After that PR, running lake exe style --update will add the exception; no more manual editing necessary.

[Michael Rothgang]

Pietro Monticone said:

Opened #14564.

We encountered another ERR_NUM_LIN since the file contains more than 1700 lines.

Can we just add the associated style exception, Kim Morrison ?

As a reviewer I'd wonder if there's a natural better place for these lemmas. (Sometimes, things can already be split into a separate file.) If not, feel free to just add the exception.

[Pietro Monticone]

Ok, great. Thanks a lot!