Zulip Chat Archive

Stream: PR reviews

Topic: Using enorm more in mathlib

Michael Rothgang (Jul 24 2025 at 15:33):

As part of the Carleson project, efforts were made (mostly by yours truly, with contributions by Yael (including a really large PR), Eric and Oliver (a bit each) and lots of input by Floris) to use enorm more in mathlib. Lot of progress has been made, but there are still a lot of opportunities for this generalisation. This thread tracks new PRs along this endavour.

Michael Rothgang (Jul 24 2025 at 15:34):

#27419 (+139/-98): generalise one section in IntegrableOn to enorms
The generalisation is straightforward; the diff is mostly adding side conditions to integrability rewriting lemmas (which were previously automatic).

Yaël Dillies (Jul 24 2025 at 15:39):

Michael Rothgang said:

the diff is mostly adding side conditions to integrability rewriting lemmas (which were previously automatic)

Stupid question: Can they be kept automatic?

Michael Rothgang (Jul 24 2025 at 15:42):

Partially yes (I added default parameters by finiteness where possible), but they don't always fire.

Michael Rothgang (Jul 24 2025 at 19:20):

#27385 (+94/-39) weaken definiteness requirement for ENormed(Add)(Comm)Monoids
One proof far downstream had to be fixed to speed up elaboration; if anybody would like to be nerd-sniped into understanding the why, I'll be very interested in the outcome!

Michael Rothgang (Jul 25 2025 at 07:28):

#27456 (+59/-6) feat: generalise more lemmas to enorms
Should be an easy review: each commit is small and stands on its own. This PR blocks further generalisation of IntegrableOn.

Michael Rothgang (Jul 25 2025 at 07:36):

#27457 (+90/-48): feat(LocallyIntegrable): generalise the first half of the file to enorms

Michael Rothgang (Jul 25 2025 at 07:47):

#27418 feat(Intervalintegral): generalise to enorms also passes CI, but depends on 27419 above

Michael Rothgang (Jul 25 2025 at 08:18):

For people doing archeology, here is a list of merged PRs towards this transition. This is exhaustive as far as I can see: I checked all Carleson PRs, as well as all PRs mentioning enorm.

Last updated: Dec 20 2025 at 21:32 UTC