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.