redefine upperRadius

[js2357]

With the current definition of upperRadius, it will always be infinity. (Infinity will be in the set that we're taking a supremum of, due to the toReal causing infinity to be treated as 0.) This PR redefines upperRadius to avoid that problem, by taking a sup over reals instead. I think a real-valued upperRadius will also be nicer to work with.

In order for the real-valued sup to behave nicely, we need to know that the set we're taking the sup of is bounded. Our assumptions ensure that this is the case in non-trivial situations, but we might need an additional assumption to rule out trivial cases. Do any of the existing assumptions ensure that d_B is not identically 0?

[fpvandoorn]

Thanks for spotting this!

My initial thought would be to still have upperRadius in ENNReal, and define it something like this:

⨆ (r : ℝ) (h : dist_{x, r} θ (Q x) < 1), ENNReal.ofReal r

I don't know exactly when upperRadius is finite, if Q is constantly θ I presume it's infinite.
To answer your other question, the following shows that d_B is not identically 0:
https://florisvandoorn.com/carleson/docs/Carleson/Defs.html#CompatibleFunctions.localOscillation_le_cdist

[js2357]

• I've been working with upperRadius, and at least as far as the proof of Lemma 7.2.2 goes, life has been a bit easier since I made it real. Is there a reason why you want to keep it in ENNReal? So far I've only had to use it in places where reals are the natural choice.
• If Θ X is a singleton then CompatibleFunctions.localOscillation_le_cdist doesn't help. Obviously it's a really trivial case that we could rule out by adding an extra assumption, but I wanted to double-check that it wasn't somehow covered by existing assumptions before adding a new one.

[fpvandoorn]

I think it can actually happen that upperRadius is infinity, and then it's easier to work with an ENNReal version. But I'm happy to keep it in Real for now, with a comment "maybe change to ENNReal if convenient".

I don't think there is any guarantee that Θ is not singleton right now, but we could assume that if convenient. Still: I think there are many cases that upperRadius is infinity for some values of θ.

[js2357]

Yeah, I guess we can't work around the case where θ = Q x. I'll change it back to ENNReal.

[fpvandoorn]

With upperRadius in ENNReal, I would write this as

⨆ (R₁ : ℝ≥0) (x' : X) (_ : dist x x' ≤ R₁),
  ‖∫ y in {y | (nndist x' y : ℝ≥0∞) ∈ Ioo (R₁ : ℝ≥0∞) (upperRadius Q θ x')}, K x' y * f y‖ₑ

[js2357]

1. I'm not sure we want that. With the original version, the left-hand inequality of the Ioo statement has ENNReal.ofReal on both sides, so it's relatively easy to translate back to a real-valued inequality. In your new version, one side has an NNReal being cast to ENNReal and the other side has a real being cast to ENNReal. I don't have time to give it much thought right now, but it feels like that would be less convenient.
2. This isn't directly relevant to what I'm currently working on, because I think the reference to linearizedNontangentialOperator in the blueprint's proof of Lemma 7.2.2 is a mistake. I think it should be nontangentialOperator instead (as appears correctly at the end of the proof).
3. My proof is almost done now (and the heavy lifting is completely finished), so it might make more sense to discuss this after I PR it. It will include a lot of API for sets of the form {y | ENNReal.ofReal (dist x' y) ∈ Ioo r R}.

[fpvandoorn]

Oh oops, I expect that an occurrence of linearizedNontangentialOperator in chapter 7 is indeed a mistake. My bad! (See CONTRIBUTING.md for the translation of symbols.)
And I'm also not sure if what I suggested is the best option.

I do expect that ENNReal.ofReal (dist x' y) is more conventiently written as edist x' y (so my (nndist x' y : ℝ≥0∞) above should also use edist)