lemma 7.7.4

Stream: Carleson

[Edward van de Meent]

i've run into a small mismatch in formalisation... at the step of applying lt_dist (2.0.36), i need 𝓘 p ≤ 𝓘 u', but i only have (𝓘 p : Set X) ⊆ 𝓘 u' (from applying if_descendant_then_subset for (𝓘 p : Set X) ⊆ 𝓘 u and fundamental_dyadic for (𝓘 u : Set X) ⊆ 𝓘 u'). in principle we do have s (𝓘 u) ≤ s (𝓘 u'), but i don't know i can get s (𝓘 p) ≤ s (𝓘 u)

[Edward van de Meent]

another way to fix this could be that the $\subset$ in the hypothesis in (2.0.36) is meant to be formalised as ⊆ rather than ≤

[Floris van Doorn]

carleson#TileStructure.Forest.smul_four_le should give you s (𝓘 p') ≤ s (𝓘 u'), after unfolding the definition of ≤ in the Lemma statement (and you already know s (𝓘 p) ≤ s (𝓘 u')). Please add that as lemma about Forest.

[Evgenia Karunus]

Great you asked this, turned out it was exactly the lemma that I was missing in my proof too (Lemma 7.5.11).
I'll create a separate PR with this lemma so that we can both use it.

[Evgenia Karunus]

Here it is github.com/fpvandoorn/carleson/pull/237

[Edward van de Meent]

i am glad to announce the proof is sorry-free! (locally)

[Edward van de Meent]

fpvandoorn/carleson#247