Small imprecision in Lemma 8.0.1

Stream: Carleson

[Sébastien Gouëzel]

If I understand correctly, Lemma 8.0.1 is not completely true as stated in the blueprint. Note that the lemma has already been formalized, but the Lean version is slightly different from the blueprint version, for a good reason. This is not a real mathematical issue, rather a definition/presentation issue, and it can be fixed in many ways. @Floris van Doorn, I'd let you discuss with your coauthors to see which fix you would prefer to implement.

The issue in the proof is when going from (8.0.11) from (8.0.12). This uses a global Hölder bound for $\varphi$, while the assumption is only that this function is Hölder continuous on the ball B (z, R), and supported there. In most cases, these assumptions are enough to get a global Hölder control: to estimate $|\varphi(x) - \varphi(y)|$ when $x$ is inside the ball and $y$ is outside, take the point $y'$ at distance $R$ of $z$ on the segment $[x, y]$, and argue that $|\varphi(x)- \varphi(y)| = |\varphi(x)-\varphi(y')| \le C d(x,y')^\tau \le C d(x,y)^\tau$.

However, in general, there is no such point $y'$, and the argument breaks down. The counterexample is the following: Suppose that, for a super small $\epsilon$, the annulus $\{y' : R-\epsilon < \mathrm{dist} (y', z) < R+\epsilon\}$ is empty. Then the function equal to $1$ on the ball $B(z, R-\epsilon)$ and to $0$ outside of $B(z, R+\epsilon)$ is $1$-Hölder on $B(z, R)$, supported on this ball, and still its global Hölder constant is extremely bad (and blows up when $\epsilon$ tends to $0$).

[Floris van Doorn]

Ah, good point. I think we can just assume/prove that the global Holder norms are bounded, but let me indeed check with my coauthors what the best solution is.

[Sébastien Gouëzel]

A possible fix (with slightly worse constants, but otherwise the same statement): start with $\varphi$ on the ball $B(z, R)$, extend it to a global Hölder function $\varphi_1$ (with Hölder constant bounded by $4 ||\varphi||_{B(z, R)}$, using the analogue of docs#LipschitzOnWith.extend_real for Hölder, and the fact that complex are two-dimensional so no bad loss). Then, use a cutoff function equal to $1$ on $B(z, R)$ and $0$ outside of $B(z, 3R/2)$ to truncate $\varphi_1$ into a new function $\varphi_2$, still keeping good controls. The function $\varphi_2$ is globally Hölder continuous and controlled. Then apply the regularization procedure to $\varphi_2$ instead of $\varphi$ (with parameter $t/2$ to make sure that the final function is still supported in $B(z, 2R)$).

[Floris van Doorn]

Oh, that might be better, since that wouldn't affect any statements outside chapter 8 (besides some constants).

[Sébastien Gouëzel]

The cheapest fix would be to assume that $\varphi$ is supported in $B(z, R/2)$ in the statement. If that's enough for the applications, I mean.

[Sébastien Gouëzel]

Forget about my fix above, it doesn't work. So the simplest thing is really to assume in Lemma 8.0.1 that the function is supported on B(z, R) but Hölder on B(z, 2R). And same thing for Proposition 2.0.5.

[Floris van Doorn]

Lars also replied that assuming it's Hölder on B(z, 2R) is probably the easiest fix. That does/should hold in the places where we apply Prop 2.0.5.

[Sébastien Gouëzel]

ok. I'll adapt the blueprint to that, tweak the current statement of Lemma 8.0.1, and prove Proposition 2.0.5 with that assumption, if that's ok with you.

[Jeremy Tan]

OK, I've ran into this problem while trying to prove Lemma 7.4.5. The output of Prop 2.0.5 is a bound in terms of

iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (2 * (8 * D ^ s J))

But what is proven in Lemma 7.5.4 is a bound on

iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (8 * D ^ s J)

I don't see any relation between these two constants proved in the repo, and as Sébastien indicated, if holderFunction t u₁ u₂ f₁ f₂ J is discontinuous at the boundary of ball (c J) (8 * D ^ s J) the first constant could be arbitrarily large.

How can I relate these two constants?

[Jeremy Tan]

I've pushed my current progress to fpvandoorn/carleson#364

[Jeremy Tan]

Furthermore there's not even a proof that iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (2 * (8 * D ^ s J)) is actually finite

[Sébastien Gouëzel]

Is there a chance you could adapt the proof of Lemma 7.5.4 to get a bound on the norm on the bigger ball?

[Jeremy Tan]

Sébastien Gouëzel said:

Is there a chance you could adapt the proof of Lemma 7.5.4 to get a bound on the norm on the bigger ball?

No chance. The condition that x ∈ ball (c J) (8 * D ^ s J) is baked into so many preceding lemmas that I'd never be able to change them to x ∈ ball (c J) (16 * D ^ s J) without changing the core assumptions.

[Jeremy Tan]

More specifically I don't know how changing the blueprint's B(J) to ball (c J) (16 * D ^ s J) (it is currently 8 * D ^ s J) would affect things, whether anything would break

[Jeremy Tan]

Floris van Doorn said:

Lars also replied that assuming it's Hölder on B(z, 2R) is probably the easiest fix. That does/should hold in the places where we apply Prop 2.0.5.

And I thought I had been assured of this, that holderFunction as it currently is is Hölder on the 16-ball with a small additional factor

[Jeremy Tan]

Sébastien Gouëzel said:

Is there a chance you could adapt the proof of Lemma 7.5.4 to get a bound on the norm on the bigger ball?

In fact I did try that and it worked – with the exact same constant as before – in fpvandoorn/carleson#365 (this PR should just be to save my progress; I expect to copy it over to the other one in due course)

[Sébastien Gouëzel]

Awesome! Do you think you could also adapt the blueprint to correspond to the statements that you actually formalize (probably in another PR to keep things manageable)?

[Jeremy Tan]

In my past PRs I corrected the blueprint and added the proofs together, but given how harrowing this experience has been I'll do the blueprint update separately

[Jeremy Tan]

I fix the lemmas and blueprint (without proving 7.4.5) in fpvandoorn/carleson#366

[Jeremy Tan]

Sébastien Gouëzel said:

(probably in another PR to keep things manageable)?

Actually, from my past experience, Floris doesn't like PRs depending on other PRs, so fpvandoorn/carleson#364 does it all in one go

[Floris van Doorn]

I definitely don't have an issue with PRs depending on each other. But you don't have to spend extra time splitting up a single PR into many parts, in that case I'm happy review the whole thing in one go.

[Floris van Doorn]

Thanks for going through the existing lemmas and fixing their statements so that they work with the fixed version of Holder van der Corput, Jeremy!