Problems in the forest operator proposition

Stream: Carleson

[Jeremy Tan]

When Lemmas 7.7.2 and 7.7.3 are applied in the first part of the proof of Proposition 2.0.4, they need the assumption that ‖(rowSupport t j).indicator g x‖ ≤ G.indicator 1 x for all j < 2 ^ n. But g is only BoundedCompactSupport, not less than a pure indicator function; furthermore rowSupport is defined as the union of several E p, but E does not depend on G at all, so I cannot conclude that ‖(rowSupport t j).indicator g x‖ ≤ G.indicator 1 x.

I suspect there are several omissions here. Was E₁ or E₂ meant instead of E in defining rowSupport?

[Jeremy Tan]

See L617, L620 and L621 in Forests.lean in fpvandoorn/carleson#379 for where the less-than-indicator assumptions are needed

[Floris van Doorn]

Oh, that seems like a small mistake. Proposition 2.0.4 is only applied for the case that $g = 1_{G\setminus G'}$, so the easiest fix is to add the assumption $g\le 1_G$ to the Proposition. In the formalisation, this means you have to add the assumption $A\subseteq G$ to forest_operator' and forest_operator_le_volume.

[Floris van Doorn]

Lars says that another fix is to indeed replace $E$ by $E_1$ in the definition of $E_j$. That also works, and doesn't require changing Proposition 2.0.4 (but I'm fine with either option).

[Jeremy Tan]

The first half of Prop 2.0.4 (g part) is done; I used the $A \subseteq G$ fix

[Jeremy Tan]

Now I run into another logical gap in the second part (the one with the dens_2). How do I go from $\mathbf 1_{E_j}$ to $\mathbf 1_F$ so that I can apply Equation (7.7.2) of Lemma 7.7.2?

[Jeremy Tan]

this part
Screenshot_20250605_123826_Firefox.png

[Jeremy Tan]

(The notation in row-bound seems to be off as well; I have tried to correct them in my PR, both blueprint and code)

[Jeremy Tan]

fpvandoorn/carleson#379 has been updated with my current progress; I'm stuck on the above blueprint error

[Jeremy Tan]

(E also has no relation to F...)

[Jeremy Tan]

@Floris van Doorn I've completed the Prop 2.0.4 proof except the second logical gap I pointed out above ($\mathbf 1_{E_j}$ to $\mathbf 1_F$)

[Floris van Doorn]

There are indeed some steps missing in the proof. The main thing to note is that Lemma 7.2.2 is about $T^*$, while in this proof we need a bound for $T$ (I'm omitting the subscripts in this post).
We know that $T$ and $T^*$ are adjoint: $\langle Tf, g\rangle = \langle f, T^*g\rangle$, this is (roughly?): carleson#TileStructure.Forest.adjointCarlesonSum_adjoint
From that, it is not hard to show that $T1_{F}$ is adjoint to $1_{F}T^*$ (note the swap of the indicator functions). Then, from Equation 7.7.2 we get for $f$ with $|f|\le1_F$ that

$$\|1_GTf\|_2^2=\langle 1_GTf, 1_GTf\rangle = \langle Tf, 1_GTf\rangle = \langle f, T^*1_GTf\rangle\\ = \langle 1_Ff, T^*1_GTf\rangle = \langle f, 1_FT^*1_GTf\rangle\\ \le \|f\|_2 \|1_FT^*1_GTf\|_2\\ \le C \|f\|_2 \|1_GTf\|_2 \le C \|f\|_2 \|Tf\|_2$$

Here the first inequality is Cauchy-Schwarz and the second equality is 7.7.2 ($Tf$ and hence $1_GTf$ is bounded with compact support, and its support is a subset of $G$).
Now $\|Tf\|_2<\infty$, so we can cancel it from both sides of the inequality to get $\|1_GTf\|\le C * \|f\|_2$.
I'll still think about how to ensure that $Tf$ (or something similar) has support in $G$.

[Floris van Doorn]

To get our support in $G$, we use our newly added hypothesis that $|g|\le 1_G$, so we can multiply all functions in (7.7.7) by $1_G$. We can still prove the proposition from the inequalities with $1_G$ added. I'll edit the calculation above to insert $1_G$.

[Floris van Doorn]

I believe you can estimate $\|1_{E_j}T_{R_j}f\|\le \|T_{R_j}f\|$ before applying the argument I described above; I don't think they play a role anymore in this part of the argument (unless I'm missing something).

[Jeremy Tan]

All this talk about adjoints and indicators and operators, without mentioning integrals, is making my head spin

[Jeremy Tan]

There's just one little thing left: how can I be sure that $|\mathbf 1_GTf|\le\mathbf 1_G$ (as that is an assumption of Lemma 7.7.2)?

[Floris van Doorn]

Jeremy Tan said:

There's just one little thing left: how can I be sure that $|\mathbf 1_GTf|\le\mathbf 1_G$ (as that is an assumption of Lemma 7.7.2)?

I'm afraid that is only true up to a constant. Tf is bounded with compact support, so for a large enough c, $|\frac1c1_GTf|\le1_G$. With the refactor of BoundedCompactSupport, you'll have to mimic carleson#MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarleson to get a uniform bound instead of an a.e.-bound (though the proof will be essentially the same as the first field of carleson#MeasureTheory.BoundedCompactSupport.carlesonOn