Porting to Mathlib

Stream: Carleson

[Floris van Doorn]

The formalization is nearing the finish line, and open formalization tasks are not so abundant anymore. If you want to help out, another big project is moving the contents of the ToMathlib actually to Mathlib.

If you are willing to help with that, please go ahead, and make PRs to Mathlib with the content of the ToMathlib folder (preferably in relatively small chunks).
Some remarks about this:

• There is a carleson label in Mathlib, so you can tag the PRs
• Some parts of ToMathlib are not completely Mathlib-ready, and unfortunately I don't have time at the moment to go through it and mark which parts might need some cleanup first. If you are unsure, feel free to ask here. Files that only have some lemmas and have name that aligns with a Mathlib file/folder (e.g. https://github.com/fpvandoorn/carleson/blob/master/Carleson/ToMathlib/Data/ENNReal.lean ) are likely easy to port.
• One thing that would be useful as preparation, is splitting up https://github.com/fpvandoorn/carleson/blob/master/Carleson/ToMathlib/Misc.lean into separate parts that correspond to Mathlib files. (This file exists because I'm lazy and didn't put them in the correct file right away. Thanks for most contributors to be less lazy than I was!)
• Please post Mathlib porting PRs in this thread.

EDIT: We now have a Porting Dashboard!

[Jim Portegies]

I'd like to help, but was wondering, how do we want to go about attributing co-authors on commits/PRs?

[Michael Rothgang]

If there's a clear candidate, include them with a line in the commit message? (Mathlib's PR template shows the syntax.) If you're not sure, ask here/use git blame?

[Jeremy Tan]

#27056 adds some strangely missing ENNReal natural power lemmas

[James Sundstrom]

Here are the ToMathlib files that don't import any other ToMathlib files, if anyone's looking for a good place to start:

Algebra.BigOperators.Pi
Analysis.Convex.SpecificFunction.Basic
Analysis.Normed.Group.Basic
Analysis.SpecialFunctions.Pow.Deriv
Analysis.Convolution
Data.Real.ConjExponents
Data.Set.Card #27093
Data.ENNReal
Data.NNReal
MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.Function.LpSpace.ContinuousFunctions
MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Integral.Bochner.ContinuousLinearMap
MeasureTheory.Integral.Average
MeasureTheory.Integral.Lebesgue
MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.ENNReal
MeasureTheory.Measure.NNReal
MeasureTheory.Measure.Prod
MeasureTheory.Measure.Restrict #27301
Order.Chain
RealInterpolation.InterpolatedExponents
Topology.Instances.AddCircle.Defs
BoundedFiniteSupport
ENorm
Interval
MinLayer

[Yaël Dillies]

@James Sundstrom, are you aware of the "upstreaming dashboard" that I developed for my own projects? Here's how it looks: https://yaeldillies.github.io/Toric/upstreaming

[Yaël Dillies]

If you want it, I can PR it to carleson

[Rémy Degenne]

You should talk to Pietro about adding it to his LeanProject template.

[Yaël Dillies]

We already did actually, but nothing came out of it yet

[Ruben Van de Velde]

I had the vague intention of adding it to the GitHub action once my FLT pr landed, but if someone's faster, even better

[James Sundstrom]

@Yaël Dillies Not that it's up to me, but here's my opinion:

Assuming it's easy for you to set up, I'm sure people would be happy to have it. If it is inconvenient to set up, the dependency graph isn't actually too complicated, so we should be okay without it.

[Jeremy Tan]

#27148 adds Finset.mem_filter_univ, which replaces a three-lemma motif used very commonly throughout the project

[Pietro Monticone]

Yaël Dillies said:

We already did actually, but nothing came out of it yet

I would certainly welcome that, I just haven’t found the time yet. Feel free to open a PR of course!

[Floris van Doorn]

Yaël Dillies said:

James Sundstrom, are you aware of the "upstreaming dashboard" that I developed for my own projects? Here's how it looks: https://yaeldillies.github.io/Toric/upstreaming

Sorry, I forgot to reply to this earlier. I agree with James: if it's easy to set up for carleson, it would be nice to have!

[Ruben Van de Velde]

Let's try: https://github.com/fpvandoorn/carleson/pull/460

[Yaël Dillies]

Here's a PR to link to it from the landing page: fpvandoorn/carleson#461

[Ruben Van de Velde]

Turns out I missed a file: https://github.com/fpvandoorn/carleson/pull/463

[Jeremy Tan]

#27252 upstreams the lemmas in ToMathlib/Misc involving a norm and exp

[James Sundstrom]

#27301 does MeasureTheory.Measure.Restrict and MeasureTheory.Measure.SumRestrict

[Jasper Mulder-Sohn]

#27934 upstreams ToMathlib/Interval, except for lemmas which turned out to already be in Mathlib.

[Jasper Mulder-Sohn]

#28119 upstreams ToMathlib/Order/Chain

[Jasper Mulder-Sohn]

#29895 upstreams ToMathlib/MeasureTheory/Integral/IntegrableOn

[Michael Rothgang]

#30829 and #30830 (by @Ruben Van de Velde, both merged) upstream two small lemmas. Thanks!

[Michael Rothgang]

Not directly porting, but related: #30967 makes finiteness slightly more powerful.

[Michael Rothgang]

#31318 by Ruben is another small upstreaming PR

[Ruben Van de Velde]

Michael Rothgang said:

#31318 by Ruben is another small upstreaming PR

+11 -0, but took me three PRs +155 -80 to prepare :sweat_smile:

[Ruben Van de Velde]

Also #31320, though it turns out both are unused in carleson - https://github.com/fpvandoorn/carleson/pull/516

[Michael Rothgang]

Thanks a lot! I'm going over all ToMathlib files, and files disappearing before I get to them is a most welcome outcome :-)

[Michael Rothgang]

I just finished going over all files in ToMathlib: each file now has a comment describing its Upstreaming status. It should tell you if a file is ready for porting, if perhaps minor changes need to be made, or if some major questions remain before porting it to mathlib.

There is a lot of left to move everything into mathlib; help is very welcome! I you'd like to help, but are not sure how, you can

• take a look at the upstreaming dashboard --- find a file there, read the comment and go ahead if it's ready
• look at the ToMathlib files in your area, pick a file whose comment seems promising and go ahead.

Both are useful. Feel free to leave a comment here to avoid duplicating work!

[Matteo Cipollina]

While in the process of upstreaming to mathlib the Hadamard factorization theorem I have noticed that two of the files we have been using in the Divisor API, taken from Carleson (ToMathlib.Annuli and ToMathlib.Interval) have not yet been upstreamed to mathlib.
I'd be happy to help @James Sundstrom and authors of Interval to upstream, as part of this PR process, if that could help.

[Ruben Van de Velde]

Go for it (but keep the PRs small, please)

[Matteo Cipollina]

Thanks! Do you remember who was the author of the Interval file?

[Michael Rothgang]

Clicking on the blame button in github reveals that the file essentially comes from this commit, so the author should be Jasper Mulder-Sohn.

[Matteo Cipollina]

Michael Rothgang ha scritto:

Clicking on the blame button in github reveals that the file essentially comes from this commit, so the author should be Jasper Mulder-Sohn.

Ok thanks! I've opened #34200 with the only two lemmas from Interval that seems fit. The 4 transitive inclusion lemmas can be derived from Ico_subset_Ici (see doc-string in Order.Interval.Set.Basic), the others are already available in IntervalSucc file.

[Michael Rothgang]

Thanks! Can you add Jasper as a co-author properly? The PR description template should tell you how to.

[Matteo Cipollina]

Michael Rothgang ha scritto:

Thanks! Can you add Jasper as a co-author properly? The PR description template should tell you how to.

I've been unable to find Jasper's email but only his github JasperMS. @Jasper Mulder-Sohn thanks if you can help :)

[Matteo Cipollina]

#34202 first PR for Annulus

[Floris van Doorn]

In the Git log you can see his email (I'll DM it to you)

[Jasper Mulder-Sohn]

Matteo Cipollina said:

Ok thanks! I've opened #34200 with the only two lemmas from Interval that seems fit. The 4 transitive inclusion lemmas can be derived from Ico_subset_Ici (see doc-string in Order.Interval.Set.Basic), the others are already available in IntervalSucc file.

Actually both that doc-string and the more general result that you used in your proof were part of #27934. However because of the long throughput time on that one I hadn't gotten around to wrapping up the upstreaming within Carleson after the Mathlib release dropped. Unfortunately it seems that the upstreaming status of the file was not entirely accurate.

So the question is if there is sufficient merit for the less-general result using $\bot$ to also be in Mathlib. But I'll defer to Michael here.

[Michael Rothgang]

I'm sorry for missing that detail about the upstreaming status; thank you for adding the context here!

[Michael Rothgang]

I am inclined to include the special cases, but will ask for second opinions in the reviewers stream.

[Matteo Cipollina]

both are actually used in the Annulus API, in terms of LOC the additional lines created by these two specializations would still somewhat spill-out to that file

[Jasper Mulder-Sohn]

Alright, that makes sense. I guess we can use the conclusion of that PR review to wrap up the upstreaming within Carleson so that the almost-duplication/discrepancy is resolved again and we can delete the ToMathlib files.

[Michael Rothgang]

Indeed - if the mathlib conclusion is to not have Ico_subset_Ici and friends, removing them from Carleson seems like the right call. I'll happily review a PR!

[Matteo Cipollina]

last one #34219