lemma 7.7.1 forest row-decomposition

Stream: Carleson

[Edward van de Meent]

for 7.1.1 7.7.1 i have one sorry left i can't figure out... i can't figure out why the new $\mathfrak u$ is $\mathfrak T$-disjoint from the previous ones (in the proof of ∀ x:X, stackSize (t \ ⋃ i < j, t.rowDecomp i : Set _) x ≤ 2 ^ n - j)

[Edward van de Meent]

see here(old) here for my code

[Edward van de Meent]

(also beware the code is not cleaned up yet)

[Floris van Doorn]

It's very hard to understand where you are in the proof when linking to a Lean formalization, and much easier if you refer to a particular step in the blueprint.

What I think is going on: you want to show that every element x still occurring in the forest after removing j rows actually occurs in at least one element of thej-th row. And you're proving that if this is not the case, you can add a maximal element containing x to the row contradicting the maximalness of the row. The reason that this new element is disjoint follows from the axioms of the grid, since elements of the grid are comparable or disjoint: carleson#le_or_ge_or_disjoint
Since both u and t are maximal elements and not equal, they cannot be comparable.

Does that finish your proof?

PS: you might want to use the order on Grid X directly, instead of casting it to Set X, e.g. by using the following in rowDecomp_zornset
∀ u ∈ x, Maximal (· ∈ ((fun x => 𝓘 x : 𝔓 X → Grid X) '' s)) (𝓘 u)

[Edward van de Meent]

i think i don't want that order tho? the reason i need this maximality (i think) is because stackSize refers to the members of the set corresponding with a grid point

[Edward van de Meent]

i think that's why the blueprint specifies "... with inclusion maximal ${\mathcal{I}}({\mathfrak u})$." (emphasis mine)

[Edward van de Meent]

(because i seem to recall that this order is not the same as just the inclusion order?)

[Floris van Doorn]

The orders are actually quite similar: carleson#Grid.le_def
In particular, every Grid-maximal element should be Set-maximal.
But I think in this proof the difference doesn't really matter

[Edward van de Meent]

i guess i'm not quite clear if the definition refers to $\mathcal I$-disjointness or $\mathfrak T$-disjointness?

[Edward van de Meent]

carleson#le_or_ge_or_disjoint seems to refer to the former

[Floris van Doorn]

carleson#Grid.le_def talks about elements in $\mathcal{D}$, if that's what you're asking.
But I guess we're getting off track. Did the rest of my message solve the gap in your proof?

[Edward van de Meent]

Floris van Doorn said:

The reason that this new element is disjoint follows from the axioms of the grid, since elements of the grid are comparable or disjoint: carleson#le_or_ge_or_disjoint

this explains why the new element's image under $\mathcal I$ is disjoint from the images of the previous ones, but as far as i can tell (for the purposes of carleson#TileStructure.Row.pairwiseDisjoint' ) i need to explain why the new element's image under $\mathfrak T$ is disjoint from the previous ones

[Edward van de Meent]

i.e. the construction says to choose disjoint tiles (under $\mathfrak T$, implied), then the proof that this construction covers everything in $2^n$ says a certain kind of tile must be in there due to maximality of your choice, but then you need to prove that including the new tile still satisfies your constraints

[Notification Bot]

13 messages were moved here from #Carleson > Outstanding Tasks, V5 by Edward van de Meent.

[Floris van Doorn]

Yes, you're right. I made a mistake last night, confusing tiles and cubes myself.

[Floris van Doorn]

I think there is indeed a gap in the proof there. I'll ask my coauthors if they see how to fix it.

[Floris van Doorn]

Oops, this was my fault, sorry!
I wrongly translated the definition of Row into Lean. I should have written that the 𝓘(u) are disjoint, not the 𝔗(u). Also, in the first sentence of the proof of Lemma 7.7.1, the disjointness means that the 𝓘(u)s are disjoint.
The proof will be almost the same, but now you can use the dyadic property of the cubes ( carleson#le_or_ge_or_disjoint ) in the place where you got stuck

[Floris van Doorn]

I just pushed a commit fixing the definition of Row.

[Edward van de Meent]

awesome, indeed that does fix the proof :thumbs_up:

[Edward van de Meent]

actually, for this proof, i'd need $\mathcal I$ to be some sort of injective, i think? i have locally proven that indeed, if $u$ is in the jth row and both $u$ and $k$ have maximal images under $\mathcal I$ (i.e. maximal for the points remaining), their images under $\mathcal I$ are either disjoint or equal... but i'm not sure that i get to conclude that that contradicts $u\neq k$?

[Edward van de Meent]

can i somehow prove that this new $k$ is in $\mathfrak T(u)$ :thinking:

[Floris van Doorn]

$\mathcal I$ is definitely not intended to be injective.

[Floris van Doorn]

Can you state more precisely where you are in the proof? Are you still on the sentence "Thus it is contained in a cube $\mathcal{I}(u)$ in with $u\in U_j$"? What is $k$?

[Edward van de Meent]

Floris van Doorn said:

Since both u and t are maximal elements and not equal, they cannot be comparable.

this is the bit where i get stuck, since technically we're not comparing u and t but 𝓘 u and 𝓘 t

[Edward van de Meent]

i.e. we know u and t are not equal, but the maximality and disjointness are about 𝓘 u and 𝓘 t. I have managed to prove that either 𝓘 u and 𝓘 t are disjoint or equal, but i don't know how to get a contradiction in the equal case.

[Floris van Doorn]

You're considering the case where there is some x in 𝓘 u that is not in 𝓘 t for any t in the j-th row, right? So therefore, 𝓘 u = 𝓘 t is impossible.

[Floris van Doorn]

Edward van de Meent said:

this is the bit where i get stuck, since technically we're not comparing u and t but 𝓘 u and 𝓘 t

I believe the order on 𝔓 X should not be used at all in Lemma 7.7.1. EDIT: I misread what you said, we're in agreement.

[Floris van Doorn]

If you're still stuck, please write in English the argument you're giving after the sentence "[...] then it is contained in a maximal such cube." in the proof of Lemma 7.7.1, and where you're stuck.

[Edward van de Meent]

Ah, that fixes it (for real this time). Indeed, we get to assume that there exists no such t and do proof by contradiction! I missed that bit

[Edward van de Meent]

My proof is now sorry free locally, I'll polish the proof and then make a PR

[Edward van de Meent]

carleson#243