HasBoundedStrongType / WeakType formalisation

Stream: Carleson

[Jasper Mulder-Sohn]

Hi, coming to a part where I will need HasBoundedStrongType / HasBoundedWeakType. Currently these are formalised using:

• MemLp f p μ
• eLpNorm f ∞ μ < ∞
• μ (support f) < ∞

which should be equivalent to BoundedFiniteSupport f μ.

To make those changes I need to assume ENormedAddMonoid ε₁ (used deep down to prove enorm_zero so it's pretty basic).
Because this is ToMathlib territory I wanted to double check that this change is not problematic (also because it turns out to be nontrivial work). It will clean the code and call stacks up considerably.
It might also be possible to prove the result without that extra assumption but that would require changes in Mathlib as well.
Thanks in advance for your feedback on how to proceed!

PS. Just to check: lemma 10.1.6 and further (including 10.0.2) have statements about HasStrongType but I think it should be HasBoundedStrongType because the blueprint talks about bounded measurable functions. Right?

[Michael Rothgang]

Using ENormedAddMonoid should be fine - I'm been on a long path generalising mathlib lemmas away from NormedAddCommGroup and similar to *ENorm* classes.

[Michael Rothgang]

There might be mathlib lemmas which assume normed groups: in this case, feel free to move on for by copying the mathlib lemma to Carleson, changing the statement, sorrying it and proceeding with your proof.
I will get to it at some point. Feel free to ping me (or prove the new lemma, if easy - makes my life easier.)

[Floris van Doorn]

Is your question whether it's ok to reformulate HasBoundedWeakType/HasBoundedStrongType so that it uses BoundedFiniteSupport? Yes, that sounds ok to me.
Ideally in the definition you only use notation classes (e.g. ENorm), but in all lemmas you can add more (e.g. ENormedAddMonoid).

[Floris van Doorn]

And yes, all three occurrences of HasStrongType in NontangentialOperator should be HasBoundedStrongType. Please PR a fix!

[Jasper Mulder-Sohn]

Floris van Doorn said:

Is your question whether it's ok to reformulate HasBoundedWeakType/HasBoundedStrongType so that it uses BoundedFiniteSupport? Yes, that sounds ok to me.
Ideally in the definition you only use notation classes (e.g. ENorm), but in all lemmas you can add more (e.g. ENormedAddMonoid).

Alright I'll get to it, thanks.

[Jasper Mulder-Sohn]

Michael Rothgang said:

There might be mathlib lemmas which assume normed groups: in this case, feel free to move on for by copying the mathlib lemma to Carleson, changing the statement, sorrying it and proceeding with your proof.
I will get to it at some point. Feel free to ping me (or prove the new lemma, if easy - makes my life easier.)

Will do, thanks!

[Jasper Mulder-Sohn]

Floris van Doorn said:

And yes, all three occurrences of HasStrongType in NontangentialOperator should be HasBoundedStrongType. Please PR a fix!

I can do that, but it might take a little bit due to other IRL priorities. Feel free to beat me to it!

[Michael Rothgang]

carleson#339

[Michael Rothgang]

Interesting, that points to the docs instead. (I would have expected PRs... though that's less useful.)

[Michael Rothgang]

Let me try again: https://github.com/fpvandoorn/carleson/pull/339

[Floris van Doorn]

Thanks!
(btw: fpvandoorn/carleson#339 is a linkifier that works for any Github repo)