Hardy-Littlewood maximal principle for countable many balls

Stream: Carleson

[Floris van Doorn]

The blueprint and formalization currently only proof the Hardy-Littlewood maximal principle for a finite collection of balls. We also need a part of this for countably many balls later, which is done in the blueprint using the monotone convergence theorem.
However, we can generalize the results a bit so that everything works well for countable collections. This is a little trickier since countable suprema can be infinite. And indeed, the Hardy-Littlewood maximal function can be infinite on a set of measure 0.

This requires some changes:
(1) carleson#MeasureTheory.SubadditiveOn.biSup should be generalized so that hT hold only almost everywhere, not everywhere.
(2) This also requires that carleson#MeasureTheory.SubadditiveOn gets changed to be true only almost everywhere
(3) We also have to show that the Hardy-Littlewood maximal function is infinite only on a set of measure 0. This should follow from the fact that is has weak type (1,1), i.e. carleson#HasWeakType.MB_one. However, that is not currently the case, because the way we formulate this result is by using docs#ENNReal.toReal, so we're losing information about where the function is infinite.
(4) To properly do this, we would like to have generalize docs#MeasureTheory.Memℒp and carleson#MeasureTheory.HasWeakType to also support codomain ENNReal. Currently it's only stated for normed groups. This generalization is possible (see this branch), since we only need that the codomain has a norm to ENNReal, which can just be the identity function if the codomain is already ENNReal.

Point (4) requires major changes in Mathlib, and I'm not sure how nice that is: probably many lemmas about normed groups don't generalize well to ENNReal, and it probably also requires adding some type-classes about precisely the behavior that both ENNReal + NormedAddCommGroup satisfy w.r.t. addition, scalar multiplication and the norm function. So maybe we should just do (3) directly, without doing (4) first.
I'll create new tasks for these steps.

[Floris van Doorn]

There are some updates here: docs#ENorm has been added to Mathlib and all definitions like MemLp and Integrable are now using them, but very few Mathlib lemmas. The Carleson project is now also heavily using this, and we can state that an operator with codomain ENNReal has weak or strong type (p,q) carleson#MeasureTheory.HasWeakType / carleson#MeasureTheory.HasStrongType
However:

1. For many lemmas we need more than ENorm, and we need classes like carleson#ENormedSpace (not to be confused with docs#ENormedSpace, which should probably be removed).
2. The real interpolation theorem still doesn't work for functions into ENNReal, and we're still stating in the Carleson project a lot that someOperator . . |>.toReal has weak/strong type, which doesn't say anything about how often someOperator is infinity. However, we have lemmas like carleson#MeasureTheory.hasWeakType_toReal_iff which transition between the two statements.

To get this to a satisfactory condition, there are a few things that need to be done, but these have nontrivial (circular?) dependencies on each other, and so far I've mostly been doing these myself, but help would be appreciated (and various of these tasks don't require deep mathematical knowledge).

Tasks (I've incorporated these tasks as 111-117 on the main list, look there for the current status):

E1: Remove toReal from all statements that someOperator . . |>.toReal have weak/strong type. Use docs#MeasureTheory.hasWeakType_toReal_iff and variants to fix proofs, possibly by including some sorries.
E2: Generalize all Mathlib lemmas about MemLp and similar definitions (see changes of #20122 for all "similar definitions") that hold for ENorm to ENorm.
E3: Upstream https://florisvandoorn.com/carleson/docs/Carleson/ToMathlib/ENorm.html (we might need to discuss if we're happy with these exact classes)
E4: Generalize all Mathlib lemmas that can be generalized to one of the classes in E3 to the appropriate class. (depends on E3)
E5: Generalize all results in WeakType.lean to ENorm-classes (depends partly on E4)
E6: Generalize the proof of the real interpolation theorem to also include operators mapping into ENNReal A start of this has been made in #209 (depends partly on E2, E4)
E7: Fix all sorry's introduced in E1. (depends on E5, E6)

[Floris van Doorn]

There is one other task that I didn't foresee here. I tried to prove the boundedness of the Hardy-Littlewood maximal function right away for countable families of balls, whereas the blueprint does it for finitely many balls first, and then generalizes it to countably many balls by considering finite subfamilies of balls that exhaust all the countably many balls.

There was one thing that I didn't realize, and that is that the Vitali covering lemma requires that the radii of the balls are bounded above, and so now the boundedness of the maximal function (carleson#hasStrongType_maximalFunction) depends on this extra condition. However, we need to get the result even in the case that the balls are not bounded above. So there is one more task:

E8: Prove carleson#hasStrongType_maximalFunction without the assumption hR that the radii of the balls are bounded above. A proof for basically this result is given in Chapter 9, everything following after equation (9.0.36).

(E7 + E8 should complete task 109)

[Michael Rothgang]

Mathlib PR #20806 might also be related. Yael is slowly fixing this; I'm reviewing it. Should land "soon".

[Yaël Dillies]

ETA for landing: maybe 4-5 days?

[Floris van Doorn]

Oh, that is nice. Thanks for doing that Yael!

[Michael Rothgang]

I should add: that PR is really boiling the mathlib ocean, it feels like it changes every single lemma statement using \norm_+ to enorms. This is really nice, thanks a lot!

[Yaël Dillies]

Yes, I am starting to think that ‖·‖ₑ was the right object all along, and ‖·‖₊ merely an usurpator :thinking:

[Michael Rothgang]

I have started working on E2

[Floris van Doorn]

I incorporated this list into the V5 task list, where I'll keep track of who is working on what.

[Michael Rothgang]

Let me note some PRs, to they don't get forgotten:

• #21380 should be easy to review (just generalises co-domains of lemmas)
• #21423 fixes a pre-existing issue (awaiting CI; should be easy to review)
• #21422 adds the first classes to mathlib (ContinuousENorm and ENormed{Add,}{Comm,}Monoid: relevant lemmas were used with to_additive quite a bit, so I think we also need the multiplicative ones.

[Michael Rothgang]

#21422 fails CI, as it causes the simpNF linter to time out in a far later file (for no reason I find obvious). How would I even start diagnosing this? I'll ask elsewhere on zulip.

[Kevin Buzzard]

Try variable ... in #synth I.IsPrime in both your branch and on master (in e.g. a fresh clone of mathlib master so you don't have to keep switching between branches) at the point of failure and see if there's any difference. IF necessary bump up the heartbeat count; see if you can get it to succeed, and then set_option Meta.trace.synthInstance true or whatever it's called, and see if you can spot the chaos that your PR may have caused by looking at the difference between the two traces.

[Michael Rothgang]

Current blocker: #22215 fixes another simpNF linter time-out. I just maintainer merge'd it; this blocks #21422.

[Jeremy Tan]

That's merged

[Michael Rothgang]

#21422 was just merged :tada:, I am working on getting #21712 ready for review now

[Michael Rothgang]

Next PR ready for review is #22708

[Michael Rothgang]

#22798 is another little PR, generalising a few lemmas