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 :-)