Generalising WeakType to ENorm

Stream: Carleson

[Michael Rothgang]

I'm looking at generalising WeakType.lean to use enorms everywhere. distribution_smul_left generalises fine to any ENormedSpace and scalar multiplication w.r.t. NNReal - but to even state HasStrongType.const_smul using enorms, I need to change HasStrongType to take an ENNReal parameter c. (For HasStrongType (k • T) p p' μ ν (‖k‖ₑ * c)to even make sense, the last parameter must be an ENNReal` - as the enorm is an ennreal. Another option could be to always prove that the product is not infinite, which seems tedious.)

Any downsides to doing so?

[Michael Rothgang]

(I can just try that out tomorrow and report back.)

[Floris van Doorn]

I'm happy to make c an ENNReal. I think it indeed makes sense to make that change.
The change would probably mean that some lemmas get a c \ne \top assumption, which is fine.

[Edward van de Meent]

we could even give those assumptions a default value of by finiteness

[Michael Rothgang]

Current mathlib PRs generalising lemmas to enorm: #24343 and #24355 (both ready for review)

[Michael Rothgang]

#24352 (depending on these) will cover the added lemmas in Carleson#313 which just were mathlib generalisations.

[Michael Rothgang]

#24356 is now ready for review, another 50-100 lines of generalising typeclasses

[Michael Rothgang]

#24481 and #24482 are two more PRs generalising. The first is easy (less than 10 lines), the other also 50-100 lines.

[Michael Rothgang]

#24640 is the next PR in the sequence

[Michael Rothgang]

Current PRs are #24820 and #24839. (Another one was merged this morning.)

[Michael Rothgang]

Generalising integral lemma, I wonder: in #24352, docs#integrableOn_const takes a hypothesis about the constant being finite. (This could be relaxed, but some condition is needed.) This means all call sites need to be adjusted for this; this commit shows there are currently 18 of them. The fix is usually very mechanical (add enorm_ne_top, perhaps with the implicit argument omitted). Should I try to automate this?

[Michael Rothgang]

I could imagine

• using by apply enorm_ne_top as a default parameter, which would probably solve ~10 of these sites
• improving finiteness and using by finiteness instead. Currently, finiteness cannot solve this --- and this might have a performance cliff (because that's what aesop sometimes does)
• deciding that quite a few of these call sites will be generalised to enorms anyway, and just proceed.

Thoughts?

[Floris van Doorn]

enorm_ne_top (actually probably its lt version, but I would have to check which is better) should definitely be added to the finiteness rule-set. There should be almost no cost to that. And using by finiteness is definitely preferred over applying a specific lemma.

Whether we want to populate all/many non-infinity side-conditions in the measure theory library is a good question. This is broader than the current refactor: there are already plenty of such side-conditions in Mathlib, so probably that discussion should be held in #mathlib4 (feel free to start this!)
I think that would be a nice change.

[Michael Rothgang]

Looking at the documentation, I found that finiteness does not run simp within aesop - which clarifies why this should be performance-neutral. :tada:

[Michael Rothgang]

I added enorm_lt_top to the finiteness rule-set and used that as a default parameter. Overall, the PR is a (small) speed-up, and it's ready for review. (Not blocking urgent work.)

[Michael Rothgang]

By the way: #25086 upstreams Carleson's finiteness tagging to mathlib. (#25111 on top of that uses finiteness to golf lots of mathlib proofs.)

[Jeremy Tan]

fpvandoorn/carleson#373 makes some progress relating to Task 117 (of course this does not constitute a claim)