The last bound

Stream: Carleson

[Jeremy Tan]

Theorem 1.0.2's proof ends with

The assumption (1.0.23) however is weaker than the assumption (1.0.18) of Theorem 1.0.2. Indeed, setting for fixed $x,\vartheta$ the outer radius $R_2=R_Q(\vartheta,x')$ shows that (1.0.21) is smaller than or equal to (1.0.16).

There is a problem: R_Q = upperRadius Q θ x' may be infinite, and $\infty$ is not a value $R_2$ can take in (1.0.16). Hence one of the sorries in fpvandoorn/carleson#435 (my PR, proving 1.0.2) is

‖∫ (y : X) in EAnnulus.oo x' (ENNReal.ofReal R₁) ⊤, K x' y * f y‖ₑ ≤
  ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖∫ (y : X) in Annulus.oo x' R₁ R₂, K x' y * f y‖ₑ

and while intuitively this seems true I don't know how to prove it. Is there something wrong or am I missing something terribly simple?

[Jeremy Tan]

This sorry is L203 in the PR as of this commit

[Jeremy Tan]

I've reduced metric_carleson to one final lemma, BST_LNT_of_BST_NT in my PR, and I have two sorries in that lemma – measurability of linearizedNontangentialOperator and the above goal. I will gladly accept any help with these two sorries :)

[Floris van Doorn]

Very nice!

carleson#CompatibleFunctions.le_cdist shows that if dist_{x₁, r} θ (Q x) > 0 then upperRadius Q θ x < ∞. If dist_{x₁, r} θ (Q x) = 0, then upperRadius will indeed be infinity... I'm not quite sure what to do in that case, let me ask Lars.

[Floris van Doorn]

This was indeed a gap. We could fix the gap by adding a small extra argument, but we decided to change the definition of $T_Q^\vartheta(x)$ instead. See this commit changing the blueprint and fpvandoorn/carleson#444. The reason is that in the blueprint we're almost everywhere working with integrals over sets with finite measure, and we also want that property in this case.
The resulting new formulation of Theorem 1.0.3 is (essentially) equivalent to the previous one.

With the new definition should make the deduction of (1.0.23) from (1.0.18) easy. Any proof that unfolds linearizedNontangentialOperator or nontangentialOperator will likely break (but hopefully can be fixed with a shorter proof).

[Jeremy Tan]

Thanks for the fix. The other sorry I mentioned (AEStronglyMeasurable linearizedNontangentialOperator) ended up being proven in exactly the same way as the existing aestronglyMeasurable_nontangentialOperator – through lower semicontinuity