7.7.2

Stream: Carleson

[Edward van de Meent]

i'm having a small bit of trouble getting past the first sentence of the proof of Lemma 7.7.2. In particular, it seems implicitly assumed that $\sum _{{\mathfrak p}\in {\mathfrak T}({\mathfrak u})} T_{{\mathfrak p}} f \leq \mathbb{1}_G$ (in order to apply Lemma 7.3.1), but i can't figure out how to get there... At the very least, it seems that the proof is omitting the $|f| \leq \mathbb{1}_G$ assumption, but even then, i'm stuck...

[Edward van de Meent]

i have this issue for proving both inequalities (7.7.3 and 7.7.4)

[Floris van Doorn]

Some of these $|f|\le1_G$ assumptions were added recently, so there might be something missing here.
So you apply Lemma 7.3.1 with $g$ (in Lemma 7.3.1) as $\sum T_pf$ but then you need to know that $|g|\le1_G$... I asked Lars for help :smile:

[James Sundstrom]

The assumption |g| <= 1_G is only being used in Lemma 7.3.1 to ensure that the support of g is contained within G. It would be trivial to change the assumption to supp(g) subset G, if that helps. (Same for the assumption about f in the second part of Lemma 7.3.1.)

[Edward van de Meent]

yea, i figured that much out as well. still, i don't know how to prove that the support of carlesonSum is in there

[Edward van de Meent]

(btw, if that's the only thing it's used for, it'd be nice if that's the concrete hypothesis for the lemma in 7.3.1)

[Floris van Doorn]

This was indeed unprovable.
https://github.com/fpvandoorn/carleson/commit/23ebef66b2852ade5c7f500db863e3ef8b6276da fixes the blueprint

[Edward van de Meent]

i think there may be another issue with the proof here... in the second equality in the chain, i seem to need $\int\|\sum_{\mathfrak{u}\in\mathfrak{U}_j} foo\|^2dx = \sum_{\mathfrak{u}\in\mathfrak{U}_j} \int \|foo\|^2 dx$... are my suspicions right that this gets fixed when relaxed to inequality?

[Jeremy Tan]

That's an application of Minkowski's inequality followed by Fubini

[Edward van de Meent]

Jeremy Tan said:

That's an application of Minkowski's inequality followed by Fubini

The fixed version, right?

[Jeremy Tan]

Yes

[Edward van de Meent]

i'm not sure minkowski quite applies here, since we need to move the square into the sum at some point, and i don't see when/how we can do that... minkowski gives this:

$$\left\|\sum_{\mathfrak{u}\in\mathfrak{U}_j} foo\right\|^2_2 \le \left(\sum_{\mathfrak{u}\in\mathfrak{U}_j} \|foo\|_2\right)^2$$

but we want to end up with this:

$$\ldots \le \sum_{\mathfrak{u}\in\mathfrak{U}_j} \|foo\|_2^2$$

In order to move the square into the sum we get left with a factor of $|\mathfrak{U}_j|$ (i think), so i think this doesn't work... and from the looks of it, when you first unfold eLpNorm you get basically the same issue?

[Edward van de Meent]

since you're integrating the norm-squared of the sum, not the sum of the norm-squareds

[Edward van de Meent]

actually maybe it's no issue since in reality there is no overlap in support per component? i'm not confident, but maybe.

[Edward van de Meent]

i managed to get through that part :tada:

[Edward van de Meent]

i've got a sorry-free proof now, it's cleanup time

[Edward van de Meent]

did the constants in 7.3.1 get increased recently?

[Edward van de Meent]

i just merged master and suddenly the bounds i had proven fail

[Edward van de Meent]

i guess i'll have to define the constants recursively (i.e. dependantly on previous constants) right now...
does (C7_3_1_1 a : ℝ≥0) * 2 ^ (a ^ 3 - n/2:ℝ) and (C7_3_1_2 a : ℝ≥0) * 2 ^ (a ^ 3 - n/2:ℝ) look good?

[Edward van de Meent]

i'm asking since the blueprint doesn't reflect the changed constants everywhere yet, particularly in the proof of 7.7.2

[Floris van Doorn]

Yes, constants get bumped sometimes. When we do that, the current workflow is that the blueprint of the lemma itself has to be changed, but we don't go through all downstream lemmas and change the value there as well (in both the theorem and the proof). So please do that yourself. In most cases it's just a matter of increasing the constant in front of the $a^3$ a bit.

I'm fine with either a recursive definition or a non-recursive definition in Lean. If it's the same amount of work for you, the recursive one might be a bit nicer since it's a bit more robust to future changes (but these are not that likely).

[Edward van de Meent]

ok, sounds good.