nitpick in 4.1.3

Stream: Carleson

[Edward van de Meent]

in the proof of the first inclusion of statement 4.1.15, one step of the proof is showing that $y' \in B(y,D^k)$ from $x \in B(y,\frac{1}{2}D^k)$ and $x\in B(y',4D^{k-1})$ using the triangle inequality and the fact that $4 \leq D$... am i missing something or is that not correct?

[Edward van de Meent]

because from what i can tell, that only allows you to show that $y' \in B(y,1\frac{1}{2}D^k)$...

[Floris van Doorn]

Note that $4 \le a$ and $D = 2 ^ {100a^2}$ so $D\gg 4$. Does that solve the issue?

[Floris van Doorn]

In this case it seems like you need $D\ge 8$.

[Edward van de Meent]

yea, i think that should do it...

[Edward van de Meent]

i'll add it as a lemma in defs, if that's alright...

[Floris van Doorn]

Yes, please add lower bounds for D that we actually use as a lemmas. Once the formalization is done (or we are much further), I'm interested in lowering certain bounds, and therefore it is convenient to use the specific value of the constants as little as possible, and instead use lemmas with bounds.

[Floris van Doorn]

Please also fix the 4s in the blueprint to the actual value you need.