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.