From 2bdc6c03a2f8d19609c6d68a4c0fd4e9b6bb5d12 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 13 Sep 2024 14:41:03 +0400
Subject: [PATCH] State lemmas in chapter 7 (#125)

Also:

* Use the simpler statement of classical Carleson as the main theorem
* Move `stackSize`
---
 CONTRIBUTING.md                           |  16 +-
 Carleson/Classical/ClassicalCarleson.lean |   8 +-
 Carleson/Discrete/Defs.lean               |   1 -
 Carleson/Discrete/Forests.lean            |  29 +-
 Carleson/FinitaryCarleson.lean            |   5 +-
 Carleson/Forest.lean                      | 142 ++---
 Carleson/ForestOperator.lean              | 610 +++++++++++++++++++---
 Carleson/HardyLittlewood.lean             |   2 +-
 Carleson/TileStructure.lean               |  44 ++
 blueprint/src/chapter/main.tex            | 142 +++--
 10 files changed, 770 insertions(+), 229 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 5ead4932..e4911181 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -37,6 +37,8 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `T_Q f(x)`       | `linearizedCarlesonOperator Q K f x` | The linearized generalized Carleson operator        |
 | `T_𝓝^θ f(x)`       | `nontangentialMaximalFunction θ f x` |   |
 | `Tₚ f(x)`       | `carlesonOn p f x`       |         |
+| `T_ℭ f(x)`       | `carlesonSum ℭ f x`       | The sum of Tₚ f(x) for p ∈ ℭ. In the blueprint only used in chapter 7, but in the formalization we will use it more.        |
+| `Tₚ* f(x)`       | `adjointCarleson p f x`       |         |
 | `e(x)`       | `Complex.exp (Complex.I * x)` |         |
 | `𝔓(I)`       | `𝓘 ⁻¹' {I}` |         |
 | `I ⊆ J`         | `I ≤ J`      | We noticed recently that we cannot (easily) assume that the coercion `Grid X → Set X` is injective. Therefore, Lean introduces two orders on `Grid X`: `I ⊆ J` means that the underlying sets satisfy this relation, and `I ≤ J` means *additionally* that `s I ≤ s J`. The order is what you should use in (almost?) all cases. |
@@ -48,8 +50,12 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `M`        | `globalMaximalFunction volume 1` |     |
 | `I_i(x)`        | `cubeOf i x` |     |
 | `R_Q(θ, x)`        | `upperRadius Q θ x` |     |
-| `S_{1,𝔲} f(x)`        | `boundaryOperator1 t u f x` |     |
-| `S_{2,𝔲} g(x)`        | `boundaryOperator2 t u g x` |     |
-| ``        | `` |     |
-| ``        | `` |     |
-| ``        | `` |     |
+| `S_{1,𝔲} f(x)`        | `boundaryOperator t u f x` |     |
+| `S_{2,𝔲} g(x)`        | `adjointBoundaryOperator t u g x` |     |
+| `𝔘`        | `t` | `t` is the (implicit) forest, sometimes `(t : Set (𝔓 X))` is required. It is equivalent to `t.𝔘` |
+| `u ∈ 𝔘`        | `u ∈ t` | `t` is the (implicit) forest, and this notation is equivalent to `u ∈ t.𝔘` |
+| `𝔗(u)`        | `t u` | `t` is the (implicit) forest, and this notation is equivalent to `t.𝔗 u`  |
+| `𝔘ⱼ`        | `rowDecomp t j` | sometimes `(rowDecomp t j : Set (𝔓 X))`    |
+| `𝔗ⱼ(u)`        | `rowDecomp t j u` |     |
+| `E`        | `E` |     |
+| `Eⱼ`        | `rowSupport t j` |     |
diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean
index 13dec313..678e174f 100644
--- a/Carleson/Classical/ClassicalCarleson.lean
+++ b/Carleson/Classical/ClassicalCarleson.lean
@@ -12,7 +12,7 @@ noncomputable section
 local notation "S_" => partialFourierSum
 
 /- Theorem 1.1 (Classical Carleson) -/
-theorem classical_carleson {f : ℝ → ℂ}
+theorem exceptional_set_carleson {f : ℝ → ℂ}
     (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π))
     {ε : ℝ} (εpos : 0 < ε) :
     ∃ E ⊆ Set.Icc 0 (2 * π), MeasurableSet E ∧ volume.real E ≤ ε ∧
@@ -105,8 +105,8 @@ theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f
     rw [one_mul]
     norm_num
 
-  -- Main step: Apply classical_carleson to get a family of exceptional sets parameterized by ε.
-  choose Eε hEε_subset _ hEε_measure hEε using (@classical_carleson f cont_f periodic_f)
+  -- Main step: Apply exceptional_set_carleson to get a family of exceptional sets parameterized by ε.
+  choose Eε hEε_subset _ hEε_measure hEε using (@exceptional_set_carleson f cont_f periodic_f)
 
   have Eεmeasure {ε : ℝ} (hε : 0 < ε) : volume (Eε hε) ≤ ENNReal.ofReal ε := by
     rw [ENNReal.le_ofReal_iff_toReal_le _ hε.le]
@@ -204,7 +204,7 @@ lemma Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P :
 end section
 
 /- Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions. -/
-theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
+theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
     ∀ᵐ x, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
   -- Reduce to a.e. convergence on [0,2π]
   apply @Function.Periodic.ae_of_ae_restrict _ Real.two_pi_pos 0
diff --git a/Carleson/Discrete/Defs.lean b/Carleson/Discrete/Defs.lean
index 99691fb2..53d35179 100644
--- a/Carleson/Discrete/Defs.lean
+++ b/Carleson/Discrete/Defs.lean
@@ -1,4 +1,3 @@
-import Carleson.Forest
 import Carleson.MinLayerTiles
 
 open MeasureTheory Measure NNReal Metric Set
diff --git a/Carleson/Discrete/Forests.lean b/Carleson/Discrete/Forests.lean
index 4d2048d7..0e257d72 100644
--- a/Carleson/Discrete/Forests.lean
+++ b/Carleson/Discrete/Forests.lean
@@ -1,4 +1,5 @@
 import Carleson.Discrete.ExceptionalSet
+import Carleson.Forest
 
 open MeasureTheory Measure NNReal Metric Complex Set
 open scoped ENNReal
@@ -128,13 +129,13 @@ lemma dens1_le_dens' {P : Set (𝔓 X)} (hP : P ⊆ TilesAt k) : dens₁ P ≤ d
     apply absurd _ this.2; use J, sl.1.trans lJ
 
 /-- Lemma 5.3.12 -/
-lemma dens1_le {A : Set (𝔓 X)} (hA : A ⊆ ℭ k n) : dens₁ A ≤ 2 ^ (4 * a - n + 1 : ℤ) :=
+lemma dens1_le {A : Set (𝔓 X)} (hA : A ⊆ ℭ k n) : dens₁ A ≤ 2 ^ (4 * (a : ℝ) - n + 1) :=
   calc
     _ ≤ dens' k A := dens1_le_dens' (hA.trans ℭ_subset_TilesAt)
     _ ≤ dens' k (ℭ (X := X) k n) := iSup_le_iSup_of_subset hA
     _ ≤ _ := by
       rw [dens'_iSup, iSup₂_le_iff]; intro p mp
-      rw [ℭ, mem_setOf] at mp; exact mp.2.2
+      rw [ℭ, mem_setOf] at mp; exact_mod_cast mp.2.2
 
 /-! ## Section 5.4 and Lemma 5.1.2 -/
 
@@ -584,14 +585,14 @@ variable (k n j l) in
 def forest : Forest X n where
   𝔘 := 𝔘₄ k n j l
   𝔗 := 𝔗₂ k n j
-  nonempty {u} hu := sorry
-  ordConnected {u} hu := forest_convex
-  𝓘_ne_𝓘 hu hp := sorry
-  smul_four_le {u} hu := forest_geometry <| 𝔘₄_subset_𝔘₃ hu
-  stackSize_le {x} := stackSize_𝔘₄_le x
-  dens₁_𝔗_le {u} hu := dens1_le <| 𝔗₂_subset_ℭ₆.trans ℭ₆_subset_ℭ
-  lt_dist hu hu' huu' p hp := forest_separation (𝔘₄_subset_𝔘₃ hu) (𝔘₄_subset_𝔘₃ hu') huu' hp
-  ball_subset hu p hp := forest_inner (𝔘₄_subset_𝔘₃ hu) hp
+  nonempty' {u} hu := sorry
+  ordConnected' {u} hu := forest_convex
+  𝓘_ne_𝓘' hu hp := sorry
+  smul_four_le' {u} hu := forest_geometry <| 𝔘₄_subset_𝔘₃ hu
+  stackSize_le' {x} := stackSize_𝔘₄_le x
+  dens₁_𝔗_le' {u} hu := dens1_le <| 𝔗₂_subset_ℭ₆.trans ℭ₆_subset_ℭ
+  lt_dist' hu hu' huu' p hp := forest_separation (𝔘₄_subset_𝔘₃ hu) (𝔘₄_subset_𝔘₃ hu') huu' hp
+  ball_subset' hu p hp := forest_inner (𝔘₄_subset_𝔘₃ hu) hp
 
 /-- The constant used in Lemma 5.1.2, with value `2 ^ (235 * a ^ 3) / (q - 1) ^ 4` -/
 -- todo: redefine in terms of other constants
@@ -600,7 +601,7 @@ def C5_1_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (235 * a ^ 3) / (q - 1) ^ 4
 lemma C5_1_2_pos : C5_1_2 a nnq > 0 := sorry
 
 lemma forest_union {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-  ∫⁻ x in G \ G', ‖∑ p ∈ { p | p ∈ 𝔓₁ }, carlesonOn p f x‖₊ ≤
+  ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖₊ ≤
     C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹  := by
   sorry
 
@@ -944,8 +945,8 @@ def C5_1_3 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (210 * a ^ 3) / (q - 1) ^ 5
 lemma C5_1_3_pos : C5_1_3 a nnq > 0 := sorry
 
 lemma forest_complement {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-  ∫⁻ x in G \ G', ‖∑ p ∈ { p | p ∉ 𝔓₁ }, carlesonOn p f x‖₊ ≤
-    C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹  := by
+  ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ᶜ f x‖₊ ≤
+    C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by
   sorry
 
 /-! ## Proposition 2.0.2 -/
@@ -960,5 +961,5 @@ variable (X) in
 theorem discrete_carleson :
     ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
     ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
-    ∫⁻ x in G \ G', ‖∑ p, carlesonOn p f x‖₊ ≤
+    ∫⁻ x in G \ G', ‖carlesonSum univ f x‖₊ ≤
     C2_0_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by sorry
diff --git a/Carleson/FinitaryCarleson.lean b/Carleson/FinitaryCarleson.lean
index 92745395..8e3a29f3 100644
--- a/Carleson/FinitaryCarleson.lean
+++ b/Carleson/FinitaryCarleson.lean
@@ -40,7 +40,7 @@ private lemma 𝔓_biUnion : @Finset.univ (𝔓 X) _ = (Icc (-S : ℤ) S).toFins
 
 private lemma sum_eq_zero_of_nmem_Icc {f : X → ℂ} {x : X} (s : ℤ)
     (hs : s ∈ (Icc (-S : ℤ) S).toFinset.filter (fun t ↦ t ∉ Icc (σ₁ x) (σ₂ x))) :
-    ∑ i ∈ Finset.filter (fun p ↦ 𝔰 p = s) Finset.univ, carlesonOn i f x = 0 := by
+    ∑ i ∈ Finset.univ.filter (fun p ↦ 𝔰 p = s), carlesonOn i f x = 0 := by
   refine Finset.sum_eq_zero (fun p hp ↦ ?_)
   simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hp
   simp only [mem_Icc, not_and, not_le, toFinset_Icc, Finset.mem_filter, Finset.mem_Icc] at hs
@@ -111,7 +111,8 @@ theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volum
   rcases discrete_carleson X with ⟨G', hG', h2G', hfG'⟩
   refine ⟨G', hG', h2G', fun f meas_f h2f ↦ le_of_eq_of_le ?_ (hfG' f meas_f h2f)⟩
   refine setLIntegral_congr_fun (measurableSet_G.diff hG') (ae_of_all volume fun x hx ↦ ?_)
-  simp_rw [tile_sum_operator hx, mul_sub, exp_sub, mul_div, div_eq_mul_inv,
+  simp_rw [carlesonSum, mem_univ, Finset.filter_True, tile_sum_operator hx, mul_sub, exp_sub,
+    mul_div, div_eq_mul_inv,
     ← smul_eq_mul (a' := _⁻¹), integral_smul_const, ← Finset.sum_smul, nnnorm_smul]
   suffices ‖(cexp (I * ((Q x) x : ℂ)))⁻¹‖₊ = 1 by rw [this, mul_one]
   simp [← coe_eq_one, mul_comm I]
diff --git a/Carleson/Forest.lean b/Carleson/Forest.lean
index 53e87b45..0f44176c 100644
--- a/Carleson/Forest.lean
+++ b/Carleson/Forest.lean
@@ -7,52 +7,9 @@ noncomputable section
 open scoped ShortVariables
 variable {X : Type*} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ}
   {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G]
-variable [TileStructure Q D κ S o] {p p' : 𝔓 X} {f g : Θ X}
+variable [TileStructure Q D κ S o] {u u' p p' : 𝔓 X} {f g : Θ X}
   {C C' : Set (𝔓 X)} {x x' : X}
 
-/-- The number of tiles `p` in `s` whose underlying cube `𝓘 p` contains `x`. -/
-def stackSize (C : Set (𝔓 X)) (x : X) : ℕ :=
-  ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator 1 x
-
-lemma stackSize_setOf_add_stackSize_setOf_not {P : 𝔓 X → Prop} :
-    stackSize {p ∈ C | P p} x + stackSize {p ∈ C | ¬ P p} x = stackSize C x := by
-  classical
-  simp_rw [stackSize]
-  conv_rhs => rw [← Finset.sum_filter_add_sum_filter_not _ P]
-  simp_rw [Finset.filter_filter]
-  congr
-
-lemma stackSize_congr (h : ∀ p ∈ C, x ∈ (𝓘 p : Set X) ↔ x' ∈ (𝓘 p : Set X)) :
-    stackSize C x = stackSize C x' := by
-  refine Finset.sum_congr rfl fun p hp ↦ ?_
-  simp_rw [Finset.mem_filter, Finset.mem_univ, true_and] at hp
-  simp_rw [indicator, h p hp, Pi.one_apply]
-
-lemma stackSize_mono (h : C ⊆ C') : stackSize C x ≤ stackSize C' x := by
-  apply Finset.sum_le_sum_of_subset (fun x ↦ ?_)
-  simp [iff_true_intro (@h x)]
-
--- Simplify the cast of `stackSize C x` from `ℕ` to `ℝ`
-lemma stackSize_real (C : Set (𝔓 X)) (x : X) : (stackSize C x : ℝ) =
-    ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator (1 : X → ℝ) x := by
-  rw [stackSize, Nat.cast_sum]
-  refine Finset.sum_congr rfl (fun u _ ↦ ?_)
-  by_cases hx : x ∈ (𝓘 u : Set X) <;> simp [hx]
-
-lemma stackSize_measurable : Measurable fun x ↦ (stackSize C x : ℝ≥0∞) := by
-  simp_rw [stackSize, Nat.cast_sum, indicator, Nat.cast_ite]
-  refine Finset.measurable_sum _ fun _ _ ↦ Measurable.ite coeGrid_measurable ?_ ?_ <;> simp
-
-/-! We might want to develop some API about partitioning a set.
-But maybe `Set.PairwiseDisjoint` and `Set.Union` are enough.
-Related, but not quite useful: `Setoid.IsPartition`. -/
-
--- /-- `u` is partitioned into subsets in `C`. -/
--- class Set.IsPartition {α ι : Type*} (u : Set α) (s : Set ι) (C : ι → Set α) : Prop :=
---   pairwiseDisjoint : s.PairwiseDisjoint C
---   iUnion_eq : ⋃ (i ∈ s), C i = u
-
-
 namespace TileStructure
 -- variable (X) in
 -- structure Tree where
@@ -71,73 +28,58 @@ variable (X) in
 /-- An `n`-forest -/
 structure Forest (n : ℕ) where
   𝔘 : Set (𝔓 X)
-  𝔗 : 𝔓 X → Set (𝔓 X) -- Is it a problem that we totalized this function?
-  nonempty {u} (hu : u ∈ 𝔘) : (𝔗 u).Nonempty
-  ordConnected {u} (hu : u ∈ 𝔘) : OrdConnected (𝔗 u) -- (2.0.33)
-  𝓘_ne_𝓘 {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : 𝓘 p ≠ 𝓘 u
-  smul_four_le {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : smul 4 p ≤ smul 1 u -- (2.0.32)
-  stackSize_le {x} : stackSize 𝔘 x ≤ 2 ^ n -- (2.0.34), we formulate this a bit differently.
-  dens₁_𝔗_le {u} (hu : u ∈ 𝔘) : dens₁ (𝔗 u : Set (𝔓 X)) ≤ 2 ^ (4 * a - n + 1 : ℤ) -- (2.0.35)
-  lt_dist {u u'} (hu : u ∈ 𝔘) (hu' : u' ∈ 𝔘) (huu' : u ≠ u') {p} (hp : p ∈ 𝔗 u')
+  𝔗 : 𝔓 X → Set (𝔓 X)
+  nonempty' {u} (hu : u ∈ 𝔘) : (𝔗 u).Nonempty
+  ordConnected' {u} (hu : u ∈ 𝔘) : OrdConnected (𝔗 u) -- (2.0.33)
+  𝓘_ne_𝓘' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : 𝓘 p ≠ 𝓘 u
+  smul_four_le' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : smul 4 p ≤ smul 1 u -- (2.0.32)
+  stackSize_le' {x} : stackSize 𝔘 x ≤ 2 ^ n -- (2.0.34), we formulate this a bit differently.
+  dens₁_𝔗_le' {u} (hu : u ∈ 𝔘) : dens₁ (𝔗 u) ≤ 2 ^ (4 * (a : ℝ) - n + 1) -- (2.0.35)
+  lt_dist' {u u'} (hu : u ∈ 𝔘) (hu' : u' ∈ 𝔘) (huu' : u ≠ u') {p} (hp : p ∈ 𝔗 u')
     (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) -- (2.0.36)
-  ball_subset {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u -- (2.0.37)
-  -- old conditions
-  -- disjoint_I : ∀ {𝔗 𝔗'}, 𝔗 ∈ I → 𝔗' ∈ I → Disjoint 𝔗.carrier 𝔗'.carrier
-  -- top_finite (x : X) : {𝔗 ∈ I | x ∈ Grid (𝓘 𝔗.top)}.Finite
-  -- card_top_le (x : X) : Nat.card {𝔗 ∈ I | x ∈ Grid (𝓘 𝔗.top) } ≤ 2 ^ n * Real.log (n + 1)
-  -- density_le {𝔗} (h𝔗 : 𝔗 ∈ I) : density G Q 𝔗 ≤ (2 : ℝ) ^ (-n : ℤ)
-  -- delta_gt {j j'} (hj : j ∈ I) (hj' : j' ∈ I) (hjj' : j ≠ j') {p : 𝔓 X} (hp : p ∈ j)
-  --   (h2p : Grid (𝓘 p) ⊆ Grid (𝓘 j'.top)) : Δ p (Q j.top) > (2 : ℝ) ^ (3 * n / δ)
-
-end TileStructure
-
---below is old
-
--- class Tree.IsThin (𝔗 : Tree X) : Prop where
---   thin {p : 𝔓 X} (hp : p ∈ 𝔗) : ball (𝔠 p) (8 * a/-fix-/ * D ^ 𝔰 p) ⊆ Grid (𝓘 𝔗.top)
+  ball_subset' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u -- (2.0.37)
 
--- alias Tree.thin := Tree.IsThin.thin
+namespace Forest
 
--- def Δ (p : 𝔓 X) (Q' : C(X, ℝ)) : ℝ := localOscillation (Grid (𝓘 p)) (𝒬 p) Q' + 1
+variable {n : ℕ} (t : Forest X n)
 
--- namespace Forest
+instance : CoeHead (Forest X n) (Set (𝔓 X)) := ⟨Forest.𝔘⟩
+instance : Membership (𝔓 X) (Forest X n) := ⟨fun t x ↦ x ∈ (t : Set (𝔓 X))⟩
+instance : CoeFun (Forest X n) (fun _ ↦ 𝔓 X → Set (𝔓 X)) := ⟨fun t x ↦ t.𝔗 x⟩
 
-/- Do we want to treat a forest as a set of trees, or a set of elements from `𝔓 X`? -/
+@[simp] lemma mem_𝔘 : u ∈ t.𝔘 ↔ u ∈ t := .rfl
+@[simp] lemma mem_𝔗 : p ∈ t.𝔗 u ↔ p ∈ t u := .rfl
 
--- instance : SetLike (Forest G Q δ n) (Tree X) where
---   coe s := s.I
---   coe_injective' p q h := by cases p; cases q; congr
+lemma nonempty (hu : u ∈ t) : (t u).Nonempty := t.nonempty' hu
+lemma ordConnected (hu : u ∈ t) : OrdConnected (t u) := t.ordConnected' hu
+lemma 𝓘_ne_𝓘 (hu : u ∈ t) (hp : p ∈ t u) : 𝓘 p ≠ 𝓘 u := t.𝓘_ne_𝓘' hu hp
+lemma smul_four_le (hu : u ∈ t) (hp : p ∈ t u) : smul 4 p ≤ smul 1 u := t.smul_four_le' hu hp
+lemma stackSize_le : stackSize t x ≤ 2 ^ n := t.stackSize_le'
+lemma dens₁_𝔗_le (hu : u ∈ t) : dens₁ (t u) ≤ 2 ^ (4 * (a : ℝ) - n + 1) := t.dens₁_𝔗_le' hu
+lemma lt_dist (hu : u ∈ t) (hu' : u' ∈ t) (huu' : u ≠ u') {p} (hp : p ∈ t u') (h : 𝓘 p ≤ 𝓘 u) :
+    2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) := t.lt_dist' hu hu' huu' hp h
+lemma ball_subset (hu : u ∈ t) (hp : p ∈ t u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u :=
+  t.ball_subset' hu hp
 
--- instance : PartialOrder (Forest G Q δ n) := PartialOrder.lift (↑) SetLike.coe_injective
+end Forest
 
--- class IsThin (𝔉 : Forest G Q δ n) : Prop where
---   thin {𝔗} (h𝔗 : 𝔗 ∈ 𝔉.I) : 𝔗.IsThin
-
--- alias thin := Forest.IsThin.thin
-
--- /-- The union of all the trees in the forest. -/
--- def carrier (𝔉 : Forest G Q δ n) : Set (𝔓 X) := ⋃ 𝔗 ∈ 𝔉.I, 𝔗
+variable (X) in
+/-- An `n`-row -/
+structure Row (n : ℕ) extends Forest X n where
+  pairwiseDisjoint' : 𝔘.PairwiseDisjoint 𝔗
 
---end Forest
+namespace Row
 
--- set_option linter.unusedVariables false in
--- variable (X) in
--- class SmallBoundaryProperty (η : ℝ) : Prop where
---   volume_diff_le : ∃ (C : ℝ) (hC : C > 0), ∀ (x : X) r (δ : ℝ), 0 < r → 0 < δ → δ < 1 →
---     volume.real (ball x ((1 + δ) * r) \ ball x ((1 - δ) * r)) ≤ C * δ ^ η * volume.real (ball x r)
+variable {n : ℕ} (t : Row X n)
 
---def boundedTiles (F : Set X) (t : ℝ) : Set (𝔓 X) :=
---  { p : 𝔓 X | ∃ x ∈ 𝓘 p, maximalFunction volume (Set.indicator F (1 : X → ℂ)) x ≤ t }
+instance : CoeHead (Row X n) (Set (𝔓 X)) := ⟨fun t ↦ t.𝔘⟩
+instance : Membership (𝔓 X) (Row X n) := ⟨fun t x ↦ x ∈ (t : Set (𝔓 X))⟩
+instance : CoeFun (Row X n) (fun _ ↦ 𝔓 X → Set (𝔓 X)) := ⟨fun t x ↦ t.𝔗 x⟩
 
--- set_option linter.unusedVariables false in
--- variable (X) in
--- class SmallBoundaryProperty (η : ℝ) : Prop where
---   volume_diff_le : ∃ (C : ℝ) (hC : C > 0), ∀ (x : X) r (δ : ℝ), 0 < r → 0 < δ → δ < 1 →
---     volume.real (ball x ((1 + δ) * r) \ ball x ((1 - δ) * r)) ≤ C * δ ^ η * volume.real (ball x r)
+@[simp] lemma mem_𝔘 : u ∈ t.𝔘 ↔ u ∈ t := .rfl
+@[simp] lemma mem_𝔗 : p ∈ t.𝔗 u ↔ p ∈ t u := .rfl
 
-/- This is defined to live in `ℝ≥0∞`. Use `ENNReal.toReal` to get a real number. -/
-/- def MB_p {ι : Type*} [Fintype ι] (p : ℝ) (ℬ : ι → X × ℝ) (u : X → ℂ) (x : X) : ℝ≥0∞ :=
-  ⨆ (i : ι) , indicator (ball (ℬ i).1 (ℬ i).2) (1 : X → ℝ≥0∞) x / volume (ball (ℬ i).1 (ℬ i).2) *
-    (∫⁻ y in (ball (ℬ i).1 (ℬ i).2), ‖u y‖₊^p)^(1/p)
+lemma pairwiseDisjoint : Set.PairwiseDisjoint t t := t.pairwiseDisjoint'
 
-abbrev MB {ι : Type*} [Fintype ι] (ℬ : ι → X × ℝ) (u : X → ℂ) (x : X) := MB_p 1 ℬ u x -/
+end Row
+end TileStructure
diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean
index 96c04b06..ca360aab 100644
--- a/Carleson/ForestOperator.lean
+++ b/Carleson/ForestOperator.lean
@@ -1,11 +1,12 @@
 import Carleson.Forest
 import Carleson.HardyLittlewood
+import Carleson.Discrete.Forests
 
 open ShortVariables TileStructure
 variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
   [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
-  {n : ℕ} {t : Forest X n} {u : 𝔓 X} {x x' : X} {G : Set (𝔓 X)} {f g : X → ℂ}
-  {I J L : Grid X}
+  {n j j' : ℕ} {t : Forest X n} {u u₁ u₂ p : 𝔓 X} {x x' : X} {𝔖 : Set (𝔓 X)}
+  {f f₁ f₂ g g₁ g₂ : X → ℂ} {I J J' L : Grid X}
 variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
 
 noncomputable section
@@ -19,50 +20,29 @@ namespace TileStructure.Forest
 
 variable (t) in
 /-- The definition `σ(u, x)` given in Section 7.1.
-We may assume `u ∈ t.𝔘` whenever proving things about this definition. -/
-def σ (u : 𝔓 X) (x : X) : Finset ℤ := .image 𝔰 { p | p ∈ t.𝔗 u ∧ x ∈ E p }
+We may assume `u ∈ t` whenever proving things about this definition. -/
+def σ (u : 𝔓 X) (x : X) : Finset ℤ := .image 𝔰 { p | p ∈ t u ∧ x ∈ E p }
 
 /- Maybe we should try to avoid using \overline{σ} and \underline{σ} in Lean:
 I don't think the set is always non-empty(?) -/
 -- def σMax (u : 𝔓 X) (x : X) : ℤ :=
---  Finset.image 𝔰 { p | p ∈ t.𝔗 u ∧ x ∈ E p } |>.max' sorry
+--  Finset.image 𝔰 { p | p ∈ t u ∧ x ∈ E p } |>.max' sorry
 
-/-- Lemma 7.1.1, freely translated. -/
-lemma convex_scales (hu : u ∈ t.𝔘) : OrdConnected (t.σ u x : Set ℤ) := sorry
-
-/-- The definition of `𝓙₀(G), defined above Lemma 7.1.2 -/
-def 𝓙₀ (G : Set (𝔓 X)) : Set (Grid X) :=
-  {J : Grid X | s J = - S ∨ ∀ p ∈ G, ¬ (𝓘 p : Set X) ⊆ ball (c J)  (100 * D ^ (s J + 1)) }
-
-/-- The definition of `𝓙(G), defined above Lemma 7.1.2 -/
-def 𝓙 (G : Set (𝔓 X)) : Set (Grid X) :=
-  {x | Maximal (· ∈ 𝓙₀ G) x}
+/-- The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2 -/
+def 𝓙₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
+  { J : Grid X | s J = - S ∨ ∀ p ∈ 𝔖, ¬ (𝓘 p : Set X) ⊆ ball (c J)  (100 * D ^ (s J + 1)) }
 
-/-- The definition of `𝓛₀(G), defined above Lemma 7.1.2 -/
-def 𝓛₀ (G : Set (𝔓 X)) : Set (Grid X) :=
-  { L : Grid X | s L = - S ∨ (∃ p ∈ G, L ≤ 𝓘 p) ∧ ∀ p ∈ G, ¬ 𝓘 p ≤ L }
-
-/-- The definition of `𝓛(G), defined above Lemma 7.1.2 -/
-def 𝓛 (G : Set (𝔓 X)) : Set (Grid X) :=
-  {x | Maximal (· ∈ 𝓛₀ G) x}
-
-/-- Part of Lemma 7.1.2 -/
-@[simp]
-lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 G, J = ⋃ I : Grid X, (I : Set X) := by
-  sorry
-
-/-- Part of Lemma 7.1.2 -/
-lemma pairwiseDisjoint_𝓙 : (𝓙 G).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
-  sorry
+/-- The definition of `𝓙(𝔖), defined above Lemma 7.1.2 -/
+def 𝓙 (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
+  { x | Maximal (· ∈ 𝓙₀ 𝔖) x}
 
-/-- Part of Lemma 7.1.2 -/
-@[simp]
-lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 G, J = ⋃ I : Grid X, (I : Set X) := by
-  sorry
+/-- The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2 -/
+def 𝓛₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
+  { L : Grid X | s L = - S ∨ (∃ p ∈ 𝔖, L ≤ 𝓘 p) ∧ ∀ p ∈ 𝔖, ¬ 𝓘 p ≤ L }
 
-/-- Part of Lemma 7.1.2 -/
-lemma pairwiseDisjoint_𝓛 : (𝓛 G).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
-  sorry
+/-- The definition of `𝓛(𝔖), defined above Lemma 7.1.2 -/
+def 𝓛 (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
+  { x | Maximal (· ∈ 𝓛₀ 𝔖) x}
 
 /-- The projection operator `P_𝓒 f(x)`, given above Lemma 7.1.3.
 In lemmas the `c` will be pairwise disjoint on `C`. -/
@@ -84,18 +64,40 @@ def nontangentialMaximalFunction (θ : Θ X) (f : X → ℂ) (x : X) : ℝ≥0
 
 variable (t) in
 /-- The operator `S_{1,𝔲} f(x)`, given in (7.1.4). -/
-def boundaryOperator1 (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
+def boundaryOperator (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
   ∑ I : Grid X, (I : Set X).indicator (x := x) fun _ ↦
-  ∑ J ∈ { J | J ∈ 𝓙 (t.𝔗 u) ∧ (J : Set X) ⊆ ball (c I) (16 * D ^ (s I)) ∧ s J ≤ s I },
+  ∑ J ∈ { J | J ∈ 𝓙 (t u) ∧ (J : Set X) ⊆ ball (c I) (16 * D ^ (s I)) ∧ s J ≤ s I },
   D ^ ((s J - s I) / a) / volume (ball (c I) (16 * D ^ (s I))) * ∫⁻ y in J, ‖f y‖₊
 
 /-- The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3. -/
 def 𝓑 : Set (ℕ × Grid X) := Icc 0 (S + 5) ×ˢ univ
 
-/-- The radius function for the collection of balls 𝓑, defined above Lemma 7.1.3. -/
+/-- The center function for the collection of balls 𝓑. -/
+def c𝓑 (z : ℕ × Grid X) : X := c z.2
+
+/-- The radius function for the collection of balls 𝓑. -/
 def r𝓑 (z : ℕ × Grid X) : ℝ := 2 ^ z.1 * D ^ s z.2
 
--- def 𝓑 : Set (Set X) := (fun (i, I) ↦ ball (c I) (2 ^ i * D ^ s I)) '' Icc 0 (S + 5) ×ˢ univ
+/-- Lemma 7.1.1, freely translated. -/
+lemma convex_scales (hu : u ∈ t) : OrdConnected (t.σ u x : Set ℤ) := sorry
+
+/-- Part of Lemma 7.1.2 -/
+@[simp]
+lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
+  sorry
+
+/-- Part of Lemma 7.1.2 -/
+lemma pairwiseDisjoint_𝓙 : (𝓙 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
+  sorry
+
+/-- Part of Lemma 7.1.2 -/
+@[simp]
+lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
+  sorry
+
+/-- Part of Lemma 7.1.2 -/
+lemma pairwiseDisjoint_𝓛 : (𝓛 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
+  sorry
 
 /-- The constant used in `first_tree_pointwise`.
 Has value `10 * 2 ^ (105 * a ^ 3)` in the blueprint. -/
@@ -103,17 +105,17 @@ Has value `10 * 2 ^ (105 * a ^ 3)` in the blueprint. -/
 def C7_1_4 (a : ℕ) : ℝ≥0 := 10 * 2 ^ (105 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.1.4 -/
-lemma first_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
+lemma first_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
     (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
     ‖∑ i in t.σ u x, ∫ y, (exp (.I * (- 𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y * f y ‖₊ ≤
-    C7_1_4 a * MB volume 𝓑 (c ·.2) r𝓑 (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' := by
+    C7_1_4 a * MB volume 𝓑 c𝓑 r𝓑 (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' := by
   sorry
 
 /-- Lemma 7.1.5 -/
-lemma second_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
+lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
     (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
-    ‖∑ i in t.σ u x, ∫ y, Ks i x y * approxOnCube (𝓙 (t.𝔗 u)) f y‖₊ ≤
-    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t.𝔗 u)) f) x' := by
+    ‖∑ i in t.σ u x, ∫ y, Ks i x y * approxOnCube (𝓙 (t u)) f y‖₊ ≤
+    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x' := by
   sorry
 
 /-- The constant used in `third_tree_pointwise`.
@@ -122,10 +124,10 @@ Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/
 def C7_1_6 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.1.6 -/
-lemma third_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
+lemma third_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
     (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
-    ‖∑ i in t.σ u x, ∫ y, Ks i x y * (f y - approxOnCube (𝓙 (t.𝔗 u)) f y)‖₊ ≤
-    C7_1_6 a * t.boundaryOperator1 u (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' := by
+    ‖∑ i in t.σ u x, ∫ y, Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y)‖₊ ≤
+    C7_1_6 a * t.boundaryOperator u (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' := by
   sorry
 
 /-- The constant used in `pointwise_tree_estimate`.
@@ -134,13 +136,13 @@ Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/
 def C7_1_3 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.1.3. -/
-lemma pointwise_tree_estimate (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
+lemma pointwise_tree_estimate (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
     (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
-    ‖∑ p ∈ { p | p ∈ t.𝔗 u }, carlesonOn p (fun y ↦ exp (.I * - 𝒬 u y) * f y) x‖₊ ≤
-    C7_1_3 a * (MB volume 𝓑 (c ·.2) r𝓑 (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' +
-    t.boundaryOperator1 u (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' +
-    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t.𝔗 u)) f) x'):= by
-  set g := approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)
+    ‖carlesonSum (t u) (fun y ↦ exp (.I * - 𝒬 u y) * f y) x‖₊ ≤
+    C7_1_3 a * (MB volume 𝓑 c𝓑 r𝓑 (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' +
+    t.boundaryOperator u (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' +
+    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x'):= by
+  set g := approxOnCube (𝓙 (t u)) (‖f ·‖)
   sorry
 
 
@@ -153,7 +155,7 @@ def C7_2_2 (a : ℕ) : ℝ≥0 := 2 ^ (103 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.2.2. -/
 lemma nontangential_operator_bound
-  (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (θ : Θ X) :
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (θ : Θ X) :
     eLpNorm (nontangentialMaximalFunction θ f · |>.toReal) 2 volume ≤ eLpNorm f 2 volume := by
   sorry
 
@@ -165,8 +167,8 @@ lemma boundary_overlap (I : Grid X) :
 
 /-- Lemma 7.2.3. -/
 lemma boundary_operator_bound
-  (hf : IsBounded (range f)) (h2f : HasCompactSupport f) {u : 𝔓 X} (hu : u ∈ t.𝔘) :
-    eLpNorm (boundaryOperator1 t u f · |>.toReal) 2 volume ≤ eLpNorm f 2 volume := by
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (hu : u ∈ t) :
+    eLpNorm (boundaryOperator t u f · |>.toReal) 2 volume ≤ eLpNorm f 2 volume := by
   sorry
 
 /-- The constant used in `nontangential_operator_bound`.
@@ -176,39 +178,510 @@ def C7_2_1 (a : ℕ) : ℝ≥0 := 2 ^ (104 * (a : ℝ) ^ 3)
 
 /-- Lemma 7.2.1. -/
 lemma tree_projection_estimate
-  (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
-  (hg : IsBounded (range g)) (h2g : HasCompactSupport g) {u : 𝔓 X} (hu : u ∈ t.𝔘) :
-    ‖∫ x, ∑ p ∈ t.𝔗 u, conj (g x) * carlesonOn p f x‖₊ ≤
-    C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) 2 volume *
-    eLpNorm (approxOnCube (𝓛 (t.𝔗 u)) (‖g ·‖)) 2 volume := by
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (hg : IsBounded (range g)) (h2g : HasCompactSupport g) (hu : u ∈ t) :
+    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖₊ ≤
+    C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t u)) (‖f ·‖)) 2 volume *
+    eLpNorm (approxOnCube (𝓛 (t u)) (‖g ·‖)) 2 volume := by
   sorry
 
 /-! ## Section 7.3 and Lemma 7.3.1 -/
 
+/-- The constant used in `local_dens1_tree_bound`.
+Has value `2 ^ (101 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_3_2 (a : ℕ) : ℝ≥0 := 2 ^ (101 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.3.2. -/
+lemma local_dens1_tree_bound (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) :
+    volume (L ∩ ⋃ (p ∈ t u), E p) ≤ C7_3_2 a * dens₁ (t u) * volume (L : Set X) := by
+  sorry
+
+/-- The constant used in `local_dens2_tree_bound`.
+Has value `2 ^ (200 * a ^ 3 + 19)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+-- feel free to modify the constant to something simpler.
+def C7_3_3 (a : ℕ) : ℝ≥0 := 2 ^ (201 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.3.3. -/
+lemma local_dens2_tree_bound (hJ : J ∈ 𝓙 (t u)) {q : 𝔓 X} (hq : q ∈ t u)
+    (hJq : ¬ Disjoint (J : Set X) (𝓘 q)) :
+    volume (F ∩ J) ≤ C7_3_3 a * dens₂ (t u) * volume (J : Set X) := by
+  sorry
+
+/-- The constant used in `density_tree_bound1`.
+Has value `2 ^ (155 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_3_1_1 (a : ℕ) : ℝ≥0 := 2 ^ (155 * (a : ℝ) ^ 3)
+
+/-- First part of Lemma 7.3.1. -/
+lemma density_tree_bound1
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (hg : IsBounded (range g)) (h2g : HasCompactSupport g) (hu : u ∈ t) :
+    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖₊ ≤
+    C7_3_1_1 a *  dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume := by
+  sorry
+
+/-- The constant used in `density_tree_bound2`.
+Has value `2 ^ (256 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_3_1_2 (a : ℕ) : ℝ≥0 := 2 ^ (256 * (a : ℝ) ^ 3)
+
+/-- Second part of Lemma 7.3.1. -/
+lemma density_tree_bound2
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (h3f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
+    (hg : IsBounded (range g)) (h2g : HasCompactSupport g) (hu : u ∈ t) :
+    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖₊ ≤
+    C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ *
+    eLpNorm f 2 volume * eLpNorm g 2 volume := by
+  sorry
+
+/-! ## Section 7.4 except Lemmas 4-6 -/
+
+/-- The definition of `Tₚ*g(x), defined above Lemma 7.4.1 -/
+def adjointCarleson (p : 𝔓 X) (f : X → ℂ) (x : X) : ℂ :=
+  ∫ y in E p, conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y
+
+/-- The definition of `T_ℭ*g(x), defined at the bottom of Section 7.4 -/
+def adjointCarlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
+  ∑ p ∈ {p | p ∈ ℭ}, adjointCarleson p f x
+
+variable (t) in
+/-- The operator `S_{2,𝔲} f(x)`, given above Lemma 7.4.3. -/
+def adjointBoundaryOperator (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
+  ‖adjointCarlesonSum (t u) f x‖₊ + MB volume 𝓑 c𝓑 r𝓑 f x + ‖f x‖₊
+
+variable (t u₁ u₂) in
+/-- The set `𝔖` defined in the proof of Lemma 7.4.4.
+We append a subscript 0 to distinguish it from the section variable. -/
+def 𝔖₀ : Set (𝔓 X) := { p ∈ t u₁ ∪ t u₂ | 2 ^ ((Z : ℝ) * n / 2) ≤ dist_(p) (𝒬 u₁) (𝒬 u₂) }
+
+/-- Part 1 of Lemma 7.4.1.
+Todo: update blueprint with precise properties needed on the function. -/
+lemma adjoint_tile_support1 (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    adjointCarleson p f =
+    (ball (𝔠 p) (5 * D ^ 𝔰 p)).indicator (adjointCarleson p ((𝓘 p : Set X).indicator f)) := by
+  sorry
+
+/-- Part 2 of Lemma 7.4.1.
+Todo: update blueprint with precise properties needed on the function. -/
+lemma adjoint_tile_support2 (hu : u ∈ t) (hp : p ∈ t u)
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    adjointCarleson p f =
+    (𝓘 p : Set X).indicator (adjointCarleson p ((𝓘 p : Set X).indicator f)) := by
+  sorry
+
+/-- The constant used in `adjoint_tree_estimate`.
+Has value `2 ^ (155 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_4_2 (a : ℕ) : ℝ≥0 := 2 ^ (155 * (a : ℝ) ^ 3)
 
+/-- Lemma 7.4.2. -/
+lemma adjoint_tree_estimate (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    eLpNorm (adjointCarlesonSum (t u) f) 2 volume ≤
+    C7_4_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by
+  sorry
+
+/-- The constant used in `adjoint_tree_control`.
+Has value `2 ^ (156 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_4_3 (a : ℕ) : ℝ≥0 := 2 ^ (155 * (a : ℝ) ^ 3)
 
-/-! ## Section 7.4 and Lemma 7.4.4 -/
+/-- Lemma 7.4.3. -/
+lemma adjoint_tree_control (hu : u ∈ t) (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    eLpNorm (adjointBoundaryOperator t u f · |>.toReal) 2 volume ≤
+    C7_4_3 a * eLpNorm f 2 volume := by
+  sorry
+
+/-- Part 2 of Lemma 7.4.7. -/
+lemma 𝔗_subset_𝔖₀ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) : t u₁ ⊆ 𝔖₀ t u₁ u₂ := by
+  sorry
+
+/-- Part 1 of Lemma 7.4.7. -/
+lemma overlap_implies_distance (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₁ ∪ t u₂)
+    (hpu₁ : ¬ Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by
+  sorry
 
+/-! ## Section 7.5 -/
+
+variable (t u₁ u₂) in
+/-- The definition `𝓙'` at the start of Section 7.5.1.
+We use a different notation to distinguish it from the 𝓙' used in Section 7.6 -/
+def 𝓙₅ : Set (Grid X) := 𝓙 (𝔖₀ t u₁ u₂) ∩ Iic (𝓘 u₁)
+
+/-- The definition of χ-tilde, defined in the proof of Lemma 7.5.2 -/
+def χtilde (J : Grid X) (x : X) : ℝ≥0 :=
+  8 - D ^ (- s J) * dist x (c J) |>.toNNReal
+
+variable (t u₁ u₂) in
+/-- The definition of χ, defined in the proof of Lemma 7.5.2 -/
+def χ (J : Grid X) (x : X) : ℝ≥0 :=
+  χtilde J x / ∑ J' ∈ { I | I ∈ 𝓙₅ t u₁ u₂ }, χtilde J' x
+
+-- /-- The definition of `B`, defined in (7.5.1) -/
+-- protected def _root_.Grid.ball (I : Grid X) : Set X := ball (c I) (8 * D ^ s I)
+
+variable (t u₁ u₂) in
+/-- The definition of h_J, defined in the proof of Section 7.5.2 -/
+def holderFunction (f₁ f₂ : X → ℂ)  (J : Grid X) (x : X) : ℂ :=
+  χ t u₁ u₂ J x * (exp (.I * 𝒬 u₁ x) * adjointCarlesonSum (t u₁) f₁ x) *
+  conj (exp (.I * 𝒬 u₂ x) * adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x)
 
-/-! ### Section 7.5 -/
 /-! ### Subsection 7.5.1 and Lemma 7.5.2 -/
 
+/-- Part of Lemma 7.5.1. -/
+lemma union_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :
+    ⋃ J ∈ 𝓙₅ t u₁ u₂, (J : Set X) = 𝓘 u₁ := by
+  sorry
+
+/-- Part of Lemma 7.5.1. -/
+lemma pairwiseDisjoint_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :
+    (𝓙₅ t u₁ u₂).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
+  sorry
+
+/-- Lemma 7.5.3 (stated somewhat differently). -/
+lemma moderate_scale_change (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hJ' : J' ∈ 𝓙₅ t u₁ u₂)
+  (h : ¬ Disjoint (J : Set X) J') : s J + 1 ≤ s J' := by
+  sorry
+
+/-- The constant used in `dist_χ_χ_le`.
+Has value `2 ^ (226 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_2 (a : ℕ) : ℝ≥0 := 2 ^ (226 * (a : ℝ) ^ 3)
+
+/-- Part of Lemma 7.5.2. -/
+lemma sum_χ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (x : X) :
+    ∑ J ∈ { I | I ∈ 𝓙₅ t u₁ u₂ }, χ t u₁ u₂ J x = (𝓘 u₁ : Set X).indicator 1 x := by
+  sorry
+
+/-- Part of Lemma 7.5.2. -/
+lemma χ_mem_Icc (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hx : x ∈ 𝓘 u₁) :
+    χ t u₁ u₂ J x ∈ Icc 0 ((ball (c I) (8 * D ^ s I)).indicator 1 x) := by
+  sorry
+
+/-- Part of Lemma 7.5.2. -/
+lemma dist_χ_χ_le (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hx : x ∈ 𝓘 u₁) (hx' : x' ∈ 𝓘 u₁) :
+    dist (χ t u₁ u₂ J x) (χ t u₁ u₂ J x) ≤ C7_5_2 a * dist x x' / D ^ s J := by
+  sorry
 
 
 /-! ### Subsection 7.5.2 and Lemma 7.5.4 -/
 
+/-- The constant used in `holder_correlation_tile`.
+Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_5 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.5.5. -/
+lemma holder_correlation_tile (hu : u ∈ t) (hp : p ∈ t u)
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    nndist (exp (.I * 𝒬 u x) * adjointCarleson p f x)
+      (exp (.I * 𝒬 u x') * adjointCarleson p f x') ≤
+    C7_5_5 a / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *
+    (nndist x x' / D ^ (𝔰 p : ℝ)) ^ (a : ℝ)⁻¹ * ∫⁻ x in E p, ‖f x‖₊ := by
+  sorry
+
+/-- Lemma 7.5.6. -/
+lemma limited_scale_impact (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
+    (h : ¬ Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) :
+    𝔰 p ∈ Icc (s J) (s J + 3) := by
+  sorry
+
+/-- The constant used in `local_tree_control`.
+Has value `2 ^ (104 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_7 (a : ℕ) : ℝ≥0 := 2 ^ (104 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.5.7. -/
+lemma local_tree_control (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    ⨆ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f x‖₊ ≤
+    C7_5_7 a * ⨅ x ∈ J, MB volume 𝓑 c𝓑 r𝓑 (‖f ·‖) x := by
+  sorry
+
+/-- Lemma 7.5.8. -/
+lemma scales_impacting_interval (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hp : p ∈ t u₁ ∪ (t u₂ ∩ 𝔖₀ t u₁ u₂))
+    (h : ¬ Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J))) : s J ≤ 𝔰 p := by
+  sorry
+
+/-- The constant used in `global_tree_control1_1`.
+Has value `2 ^ (154 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_9_1 (a : ℕ) : ℝ≥0 := 2 ^ (154 * (a : ℝ) ^ 3)
+
+/-- The constant used in `global_tree_control1_2`.
+Has value `2 ^ (153 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_9_2 (a : ℕ) : ℝ≥0 := 2 ^ (153 * (a : ℝ) ^ 3)
+
+/-- Part 1 of Lemma 7.5.9 -/
+lemma global_tree_control1_1 (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (ℭ : Set (𝔓 X)) (hℭ : ℭ = t u₁ ∨ ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂)
+    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    ⨆ x ∈ ball (c J) (8 * D ^ s J), ‖adjointCarlesonSum ℭ f x‖₊ ≤
+    (⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum ℭ f x‖₊) +
+    C7_5_9_1 a * ⨅ x ∈ J, MB volume 𝓑 c𝓑 r𝓑 (‖f ·‖) x := by
+  sorry
+
+/-- Part 2 of Lemma 7.5.9 -/
+lemma global_tree_control1_2 (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (ℭ : Set (𝔓 X)) (hℭ : ℭ = t u₁ ∨ ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂)
+    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (hx : x ∈ ball (c J) (8 * D ^ s J)) (hx' : x' ∈ ball (c J) (8 * D ^ s J)) :
+    nndist (exp (.I * 𝒬 u x) * adjointCarlesonSum ℭ f x)
+      (exp (.I * 𝒬 u x') * adjointCarlesonSum ℭ f x') ≤
+    C7_5_9_1 a * (nndist x x' / D ^ (𝔰 p : ℝ)) ^ (a : ℝ)⁻¹ *
+    ⨅ x ∈ J, MB volume 𝓑 c𝓑 r𝓑 (‖f ·‖) x := by
+  sorry
+
+/-- The constant used in `global_tree_control2`.
+Has value `2 ^ (155 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_10 (a : ℕ) : ℝ≥0 := 2 ^ (155 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.5.10 -/
+lemma global_tree_control2 (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    ⨆ x ∈ ball (c J) (8 * D ^ s J), ‖adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f x‖₊ ≤
+    ⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂) f x‖₊ +
+    C7_5_10 a * ⨅ x ∈ J, MB volume 𝓑 c𝓑 r𝓑 (‖f ·‖) x := by
+  sorry
+
+/-- The constant used in `holder_correlation_tree`.
+Has value `2 ^ (535 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_4 (a : ℕ) : ℝ≥0 := 2 ^ (535 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.5.4. -/
+lemma holder_correlation_tree (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    HolderOnWith (C7_5_4 a *
+    ((⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₁) f₁ x‖₊) +
+    (⨅ x ∈ J, MB volume 𝓑 c𝓑 r𝓑 (‖f₁ ·‖) x).toNNReal) *
+    ((⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂) f₂ x‖₊) +
+    (⨅ x ∈ J, MB volume 𝓑 c𝓑 r𝓑 (‖f₂ ·‖) x).toNNReal))
+    nnτ (holderFunction t u₁ u₂ f₁ f₂ J) (ball (c J) (8 * D ^ s J)) := by
+  sorry
 
 
 /-! ### Subsection 7.5.3 and Lemma 7.4.5 -/
 
+/-- The constant used in `lower_oscillation_bound`.
+Has value `2 ^ (Z * n / 2 - 201 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_5_11 (a n : ℕ) : ℝ≥0 := 2 ^ (Z * n / 2 - 201 * (a : ℝ) ^ 3)
 
+/-- Lemma 7.5.11 -/
+lemma lower_oscillation_bound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) :
+    C7_5_11 a n ≤ dist_{c J, 8 * D ^ s J} (𝒬 u₁) (𝒬 u₂) := by
+  sorry
+
+/-- The constant used in `correlation_distant_tree_parts`.
+Has value `2 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3))` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_4_5 (a n : ℕ) : ℝ≥0 := 2 ^ (541 * (a : ℝ) ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3))
+
+/-- Lemma 7.4.5 -/
+lemma correlation_distant_tree_parts (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) g₂ x)‖₊ ≤
+    C7_4_5 a n *
+    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) · |>.toReal) 2 volume *
+    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) · |>.toReal) 2 volume := by
+  sorry
 
 /-! ## Section 7.6 and Lemma 7.4.6 -/
 
+variable (t u₁) in
+/-- The definition `𝓙'` at the start of Section 7.6.
+We use a different notation to distinguish it from the 𝓙' used in Section 7.5 -/
+def 𝓙₆ : Set (Grid X) := 𝓙 (t u₁) ∩ Iic (𝓘 u₁)
+
+/-- Part of Lemma 7.6.1. -/
+lemma union_𝓙₆ (hu₁ : u₁ ∈ t) :
+    ⋃ J ∈ 𝓙₆ t u₁, (J : Set X) = 𝓘 u₁ := by
+  sorry
+
+/-- Part of Lemma 7.6.1. -/
+lemma pairwiseDisjoint_𝓙₆ (hu₁ : u₁ ∈ t) :
+    (𝓙₆ t u₁).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
+  sorry
+
+/-- The constant used in `thin_scale_impact`. This is denoted `s₁` in the proof of Lemma 7.6.3.
+Has value `Z * n / (202 * a ^ 3) - 2` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_6_3 (a n : ℕ) : ℝ := Z * n / (202 * a ^ 3) - 2
+
+-- if needed
+lemma C7_6_3_pos [ProofData a q K σ₁ σ₂ F G] (h : 1 ≤ n) : 0 < C7_6_3 a n := by
+  sorry
+
+/-- Lemma 7.6.3. -/
+lemma thin_scale_impact (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₆ t u₁)
+    (h : ¬ Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J))) :
+    𝔰 p ≤ s J - C7_6_3 a n := by
+  sorry
+
+/-- The constant used in `square_function_count`.
+Has value `Z * n / (202 * a ^ 3) - 2` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_6_4 (a : ℕ) (s : ℤ) : ℝ≥0 := 2 ^ (104 * (a : ℝ) ^ 2) * (8 * D ^ (- s)) ^ κ
+
+/-- Lemma 7.6.4. -/
+lemma square_function_count (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ /- ? -/) :
+    ⨍⁻ x : X, (∑ I ∈ {I : Grid X | s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧
+    ¬ Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)) },
+    (ball (c I) (8 * D ^ s I)).indicator 1 x) ^ 2 ≤ C7_6_4 a s' := by
+  sorry
+
+
+
+
+/-- The constant used in `bound_for_tree_projection`.
+Has value `2 ^ (118 * a ^ 3 - 100 / (202 * a) * Z * n * κ)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_6_2 (a n : ℕ) : ℝ≥0 := 2 ^ (118 * (a : ℝ) ^ 3 - 100 / (202 * a) * Z * n * κ)
+
+/-- Lemma 7.6.2. Todo: add needed hypothesis to LaTeX -/
+lemma bound_for_tree_projection (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume ≤
+    C7_6_2 a n *
+    eLpNorm ((𝓘 u₁ : Set X).indicator (MB volume 𝓑 c𝓑 r𝓑 (‖f ·‖) · |>.toReal)) 2 volume := by
+  sorry
+
+/-- The constant used in `correlation_near_tree_parts`.
+Has value `2 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3))` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_4_6 (a n : ℕ) : ℝ≥0 := 2 ^ (222 * (a : ℝ) ^ 3 - Z * n * 2 ^ (-10 * (a : ℝ)))
+
+/-- Lemma 7.4.6 -/
+lemma correlation_near_tree_parts (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) g₂ x)‖₊ ≤
+    C7_4_6 a n *
+    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) · |>.toReal) 2 volume *
+    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) · |>.toReal) 2 volume := by
+  sorry
+
+
+/-! ## Lemmas 7.4.4 -/
+
+/-- The constant used in `correlation_separated_trees`.
+Has value `2 ^ (550 * a ^ 3 - 3 * n)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_4_4 (a n : ℕ) : ℝ≥0 := 2 ^ (550 * (a : ℝ) ^ 3 - 3 * n)
+
+lemma correlation_separated_trees_of_subset (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖₊ ≤
+    C7_4_4 a n *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) · |>.toReal) 2 volume *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) · |>.toReal) 2 volume := by
+  sorry
+
+/-- Lemma 7.4.4. -/
+lemma correlation_separated_trees (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖₊ ≤
+    C7_4_4 a n *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) · |>.toReal) 2 volume *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) · |>.toReal) 2 volume := by
+  sorry
 
 
 /-! ## Section 7.7 and Proposition 2.0.4 -/
 
+
+/-- The row-decomposition of a tree, defined in the proof of Lemma 7.7.1.
+The indexing is off-by-one compared to the blueprint. -/
+def rowDecomp (t : Forest X n) (j : ℕ) : Row X n := sorry
+
+/-- Part of Lemma 7.7.1 -/
+@[simp]
+lemma biUnion_rowDecomp : ⋃ j < 2 ^ n, t.rowDecomp j = (t : Set (𝔓 X)) := by
+  sorry
+
+/-- Part of Lemma 7.7.1 -/
+lemma pairwiseDisjoint_rowDecomp :
+    (Iio (2 ^ n)).PairwiseDisjoint (rowDecomp t · : ℕ → Set (𝔓 X)) := by
+  sorry
+
+@[simp] lemma rowDecomp_apply : t.rowDecomp j u = t u := by
+  sorry
+
+/-- The constant used in `row_bound`.
+Has value `2 ^ (156 * a ^ 3 - n / 2)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_7_2_1 (a n : ℕ) : ℝ≥0 := 2 ^ (156 * (a : ℝ) ^ 3 - n / 2)
+
+/-- The constant used in `indicator_row_bound`.
+Has value `2 ^ (257 * a ^ 3 - n / 2)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_7_2_2 (a n : ℕ) : ℝ≥0 := 2 ^ (257 * (a : ℝ) ^ 3 - n / 2)
+
+/-- Part of Lemma 7.7.2. -/
+lemma row_bound (hj : j < 2 ^ n) (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    eLpNorm (∑ u ∈ {p | p ∈ rowDecomp t j}, adjointCarlesonSum (t u) f) 2 volume ≤
+    C7_7_2_1 a n * eLpNorm f 2 volume := by
+  sorry
+
+/-- Part of Lemma 7.7.2. -/
+lemma indicator_row_bound (hj : j < 2 ^ n) (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
+    eLpNorm (∑ u ∈ {p | p ∈ rowDecomp t j}, F.indicator <| adjointCarlesonSum (t u) f) 2 volume ≤
+    C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by
+  sorry
+
+/-- The constant used in `row_correlation`.
+Has value `2 ^ (862 * a ^ 3 - 3 * n)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_7_3 (a n : ℕ) : ℝ≥0 := 2 ^ (862 * (a : ℝ) ^ 3 - 2 * n)
+
+/-- Lemma 7.7.3. -/
+lemma row_correlation (hjj' : j < j') (hj' : j' < 2 ^ n)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, (∑ u ∈ {p | p ∈ rowDecomp t j}, adjointCarlesonSum (t u) f₁ x) *
+    (∑ u ∈ {p | p ∈ rowDecomp t j'}, adjointCarlesonSum (t u) f₂ x)‖₊ ≤
+    C7_7_3 a n * eLpNorm f₁ 2 volume * eLpNorm f₂ 2 volume := by
+  sorry
+
+variable (t) in
+/-- The definition of `Eⱼ` defined above Lemma 7.7.4. -/
+def rowSupport (j : ℕ) : Set X := ⋃ (u ∈ rowDecomp t j) (p ∈ t u), E p
+
+/-- Lemma 7.7.4 -/
+lemma pairwiseDisjoint_rowSupport :
+    (Iio (2 ^ n)).PairwiseDisjoint (rowSupport t) := by
+  sorry
+
 end TileStructure.Forest
 
 /-- The constant used in `forest_operator`.
@@ -219,8 +692,7 @@ def C2_0_4 (a q : ℝ) (n : ℕ) : ℝ≥0 := 2 ^ (432 * a ^ 3 - (q - 1) / q * n
 theorem forest_operator {n : ℕ} (𝔉 : Forest X n) {f g : X → ℂ}
     (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g)
     (h2g : IsBounded (support g)) :
-    ‖∫ x, conj (g x) * ∑ u ∈ { p | p ∈ 𝔉.𝔘 },
-      ∑ p ∈ { p | p ∈ 𝔉.𝔗 u }, carlesonOn p f x‖₊ ≤
-    C2_0_4 a q n * (dens₂ (X := X) (⋃ u ∈ 𝔉.𝔘, 𝔉.𝔗 u)) ^ (q⁻¹ - 2⁻¹) *
+    ‖∫ x, conj (g x) * ∑ u ∈ { p | p ∈ 𝔉 }, carlesonSum (𝔉 u) f x‖₊ ≤
+    C2_0_4 a q n * (dens₂ (X := X) (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *
     eLpNorm f 2 volume * eLpNorm g 2 volume := by
   sorry
diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean
index b5df8bc5..480ae8c6 100644
--- a/Carleson/HardyLittlewood.lean
+++ b/Carleson/HardyLittlewood.lean
@@ -39,7 +39,7 @@ def maximalFunction (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι →
 
 /-- The Hardy-Littlewood maximal function w.r.t. a collection of balls 𝓑 with exponent 1.
 M_𝓑 in the blueprint. -/
-abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) :=
+abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) : ℝ≥0∞ :=
   maximalFunction μ 𝓑 c r 1 u x
 
 -- We will replace the criterion `P` used in `MeasureTheory.SublinearOn.maximalFunction` with the
diff --git a/Carleson/TileStructure.lean b/Carleson/TileStructure.lean
index ec608586..3ca72fd8 100644
--- a/Carleson/TileStructure.lean
+++ b/Carleson/TileStructure.lean
@@ -97,6 +97,12 @@ def carlesonOn (p : 𝔓 X) (f : X → ℂ) : X → ℂ :=
   indicator (E p)
     fun x ↦ ∫ y, exp (I * (Q x y - Q x x)) * K x y * ψ (D ^ (- 𝔰 p) * dist x y) * f y
 
+open Classical in
+/-- The operator `T_ℭ f` defined at the bottom of Section 7.4.
+We will use this in other places of the formalization as well. -/
+def carlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
+  ∑ p ∈ {p | p ∈ ℭ}, carlesonOn p f x
+
 lemma carlesonOn_def' (p : 𝔓 X) (f : X → ℂ) : carlesonOn p f =
     indicator (E p) fun x ↦ ∫ y, Ks (𝔰 p) x y * f y * exp (I * (Q x y - Q x x)) := by
   unfold carlesonOn Ks
@@ -281,3 +287,41 @@ lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) :
     IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄) ↔
     ∀ p p', p ∈ 𝔄 → p' ∈ 𝔄 → p ≠ p' →
     Disjoint (toTileLike (X := X) p).toTile (toTileLike p').toTile := sorry
+
+/-! ### Stack sizes -/
+
+variable {C C' : Set (𝔓 X)} {x x' : X}
+open scoped Classical
+
+/-- The number of tiles `p` in `s` whose underlying cube `𝓘 p` contains `x`. -/
+def stackSize (C : Set (𝔓 X)) (x : X) : ℕ :=
+  ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator 1 x
+
+lemma stackSize_setOf_add_stackSize_setOf_not {P : 𝔓 X → Prop} :
+    stackSize {p ∈ C | P p} x + stackSize {p ∈ C | ¬ P p} x = stackSize C x := by
+  classical
+  simp_rw [stackSize]
+  conv_rhs => rw [← Finset.sum_filter_add_sum_filter_not _ P]
+  simp_rw [Finset.filter_filter]
+  congr
+
+lemma stackSize_congr (h : ∀ p ∈ C, x ∈ (𝓘 p : Set X) ↔ x' ∈ (𝓘 p : Set X)) :
+    stackSize C x = stackSize C x' := by
+  refine Finset.sum_congr rfl fun p hp ↦ ?_
+  simp_rw [Finset.mem_filter, Finset.mem_univ, true_and] at hp
+  simp_rw [indicator, h p hp, Pi.one_apply]
+
+lemma stackSize_mono (h : C ⊆ C') : stackSize C x ≤ stackSize C' x := by
+  apply Finset.sum_le_sum_of_subset (fun x ↦ ?_)
+  simp [iff_true_intro (@h x)]
+
+-- Simplify the cast of `stackSize C x` from `ℕ` to `ℝ`
+lemma stackSize_real (C : Set (𝔓 X)) (x : X) : (stackSize C x : ℝ) =
+    ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator (1 : X → ℝ) x := by
+  rw [stackSize, Nat.cast_sum]
+  refine Finset.sum_congr rfl (fun u _ ↦ ?_)
+  by_cases hx : x ∈ (𝓘 u : Set X) <;> simp [hx]
+
+lemma stackSize_measurable : Measurable fun x ↦ (stackSize C x : ℝ≥0∞) := by
+  simp_rw [stackSize, Nat.cast_sum, indicator, Nat.cast_ite]
+  refine Finset.measurable_sum _ fun _ _ ↦ Measurable.ite coeGrid_measurable ?_ ?_ <;> simp
diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex
index 64cbaaa1..00a0aff7 100644
--- a/blueprint/src/chapter/main.tex
+++ b/blueprint/src/chapter/main.tex
@@ -27,7 +27,7 @@
 
 \chapter{Introduction}
 
-In \cite{carleson}, L. Carleson addressed a classical question regarding the convergence of Fourier series of continuous functions by proving their pointwise convergence almost everywhere. \Cref{classical-Carleson} represents a version of this result.
+In \cite{carleson}, L. Carleson addressed a classical question regarding the convergence of Fourier series of continuous functions by proving their pointwise convergence almost everywhere, as stated below in \Cref{classical-carleson}.
 
 Let $f$ be a complex valued, $2\pi$-periodic bounded Borel measurable function on the real line, and for an integer $n$, define the Fourier coefficient as
 \begin{equation}
@@ -39,25 +39,19 @@ \chapter{Introduction}
 \end{equation}
 
 \begin{theorem}[classical Carleson]
-    \label{classical-Carleson}
+    \label{classical-carleson}
     \leanok
     \lean{classical_carleson}
-    \uses{smooth-approximation, convergence-for-smooth,
-    control-approximation-effect}
-    Let $f$ be a $2\pi$-periodic complex-valued continuous function on $\mathbb{R}$. For all $\epsilon>0$, there exists a Borel set $E\subset [0,2\pi]$ with Lebesgue measure $|E|\le \epsilon$ and a positive integer $N_0$ such that for all $x\in [0,2\pi]\setminus E$ and all integers $N>N_0$, we have
-    \begin{equation}\label{aeconv}
-    |f(x)-S_N f(x)|\le \epsilon.
+    \uses{exceptional-set-carleson}
+    Let $f$ be a $2\pi$-periodic complex-valued continuous function on $\mathbb{R}$.
+    Then for almost all $x \in \mathbb{R}$ we have
+    \begin{equation}\label{eq:fourier_limit}
+      \lim_{n\to\infty}S_n f(x) = f(x).
     \end{equation}
+    In other words: the set of real numbers $x$ where \eqref{eq:fourier_limit} fails has Lebesgue measure $0$.
 \end{theorem}
 
-%Note that mere continuity implies uniform continuity in the setting of this theorem.
-By applying this theorem with a sequence of $\epsilon_n:= 2^{-n}\delta$ for $n\ge 1$ and taking the union
-of corresponding exceptional sets $E_n$, we see that outside a set of measure $\delta$, the partial Fourier
-sums converge pointwise for $N\to \infty$. Applying this with a sequence of $\delta$ shrinking to zero and
-taking the intersection of the corresponding exceptional sets, which has measure zero, we see that the Fourier
-series converges outside a set of measure zero.
-
-The purpose of this paper is twofold. On the one hand, it prepares computer verification of \Cref{classical-Carleson} by presenting a very detailed proof as a blueprint for coding in Lean. We pass through a bound for a generalization of the so-called Carleson operator to doubling metric measure spaces. This generalization is new, and proving these bounds constitutes the second purpose of this paper. This generalization incorporates several results from the recent literature, most prominently bounds for the polynomial Carleson operator of V. Lie \cite{lie-polynomial} as well as its generalization \cite{zk-polynomial}. A computer verification of our theorem will also entail a computer verification for the bulk of the work in these results.
+The purpose of this paper is twofold. On the one hand, it prepares computer verification of \Cref{classical-carleson} by presenting a very detailed proof as a blueprint for coding in Lean. We pass through a bound for a generalization of the so-called Carleson operator to doubling metric measure spaces. This generalization is new, and proving these bounds constitutes the second purpose of this paper. This generalization incorporates several results from the recent literature, most prominently bounds for the polynomial Carleson operator of V. Lie \cite{lie-polynomial} as well as its generalization \cite{zk-polynomial}. A computer verification of our theorem will also entail a computer verification for the bulk of the work in these results.
 
 We proceed to introduce the setup for our general theorem.
 We carry a multi purpose parameter, a natural number
@@ -2037,7 +2031,7 @@ \section{Proof of the Exceptional Sets Lemma}
     {\mu(F\cap B(\pc(\fp),r(\fp)))}\ge K{\mu(B(\pc(\fp),r(\fp)))}\, .
     $$
     This ball exists by definition of $\fP_{F,G}$
-    and $\dens_2$. By applying \Cref{Hardy-Littlewood}to the collection of balls
+    and $\dens_2$. By applying \Cref{Hardy-Littlewood} to the collection of balls
     $$
         \mathcal{B} = \{B(\pc(\fp),r(\fp)) \ : \ \fp \in \fP_{F,G}\}
     $$
@@ -3513,7 +3507,7 @@ \section{The density arguments}\label{sec-TT*-T*T}
 = 2^{255a^3+110a + 1}
  {\dens_1(\mathfrak{A})^{\frac 1p}} \int |g|(y)(M_{\mathcal{B}', p'}g)(y) \, dy\,.
          \end{equation}
-Applying Cauchy-Schwarz and using \Cref{Hardy-Littlewood}estimates the last display by
+Applying Cauchy-Schwarz and using \Cref{Hardy-Littlewood} estimates the last display by
 \begin{equation}
     2^{255a^3+110a + 1} \dens_1(\mathfrak{A})^{\frac 1p}
     \|g\|_2 \|M_{\mathcal{B}', p'} g\|_2
@@ -4755,6 +4749,8 @@ \section{The quantitative \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[densities tree bound]
     \label{densities-tree-bound}
+    \leanok
+    \lean{TileStructure.Forest.density_tree_bound1, TileStructure.Forest.density_tree_bound2}
     \uses{tree-projection-estimate,local-dens1-tree-bound,local-dens2-tree-bound}
     Let $\fu \in \fU$. Then for all $f,g$ bounded with bounded support
     \begin{equation}
@@ -4772,6 +4768,8 @@ \section{The quantitative \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[local dens1 tree bound]
     \label{local-dens1-tree-bound}
+    \leanok
+    \lean{TileStructure.Forest.local_dens1_tree_bound}
     \uses{monotone-cube-metrics}
     Let $\fu \in \fU$ and $L \in \mathcal{L}(\fT(\fu))$. Then
     \begin{equation}
@@ -4782,6 +4780,8 @@ \section{The quantitative \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[local dens2 tree bound]
     \label{local-dens2-tree-bound}
+    \leanok
+    \lean{TileStructure.Forest.local_dens2_tree_bound}
     Let $J \in \mathcal{J}(\fT(\fu))$ be such that there exist $\fq \in \fT(\fu)$ with $J \cap \scI(\fq) \ne \emptyset$. Then
     $$
         \mu(F \cap J) \le 2^{200a^3 + 19} \dens_2(\fT(\fu)) \mu(J)\,.
@@ -4948,6 +4948,8 @@ \section{Almost orthogonality of separated trees}
 
 \begin{lemma}[adjoint tile support]
     \label{adjoint-tile-support}
+    \leanok
+    \lean{TileStructure.Forest.adjoint_tile_support1, TileStructure.Forest.adjoint_tile_support2}
     For each $\fp \in \fP$, we have
     $$
         T_{\fp}^* g = \mathbf{1}_{B(\pc(\fp), 5D^{\ps(\fp)})} T_{\fp}^* \mathbf{1}_{\scI(\fp)} g\,.
@@ -4979,6 +4981,8 @@ \section{Almost orthogonality of separated trees}
 
 \begin{lemma}[adjoint tree estimate]
     \label{adjoint-tree-estimate}
+    \leanok
+    \lean{TileStructure.Forest.adjoint_tree_estimate}
     \uses{densities-tree-bound}
     For all bounded $g$ with bounded support, we have that
     $$
@@ -5004,15 +5008,17 @@ \section{Almost orthogonality of separated trees}
 $$
 \begin{lemma}[adjoint tree control]
     \label{adjoint-tree-control}
+    \leanok
+    \lean{TileStructure.Forest.adjoint_tree_control}
     \uses{adjoint-tree-estimate}
-    We have for all bounded $g$ with bounded support
+    We have for all $\fu \in \fU$ and bounded $g$ with bounded support
     $$
         \|S_{2, \fu} g\|_2 \le 2^{156a^3} \|g\|_2\,.
     $$
 \end{lemma}
 
 \begin{proof}
-    This follows immediately from Minkowski's inequality, \Cref{Hardy-Littlewood}and \Cref{adjoint-tree-estimate}, using that $a \ge 4$.
+    This follows immediately from Minkowski's inequality, \Cref{Hardy-Littlewood} and \Cref{adjoint-tree-estimate}, using that $a \ge 4$.
 \end{proof}
 
 
@@ -5020,6 +5026,8 @@ \section{Almost orthogonality of separated trees}
 
 \begin{lemma}[correlation separated trees]
     \label{correlation-separated-trees}
+    \leanok
+    \lean{TileStructure.Forest.correlation_separated_trees}
     \uses{correlation-distant-tree-parts,correlation-near-tree-parts}
     For any $\fu_1 \ne \fu_2 \in \fU$ and all bounded $g_1, g_2$ with bounded support, we have
     \begin{equation}
@@ -5046,6 +5054,8 @@ \section{Almost orthogonality of separated trees}
 
 \begin{lemma}[correlation distant tree parts]
         \label{correlation-distant-tree-parts}
+        \leanok
+        \lean{TileStructure.Forest.correlation_distant_tree_parts}
         \uses{Holder-van-der-Corput,Lipschitz-partition-unity,Holder-correlation-tree,lower-oscillation-bound}
         We have for all $\fu_1 \ne \fu_2 \in \fU$ with $\scI(\fu_1) \subset \scI(\fu_2)$ and all bounded $g_1, g_2$ with bounded support
         \begin{equation}
@@ -5059,6 +5069,8 @@ \section{Almost orthogonality of separated trees}
     \end{lemma}
     \begin{lemma}[correlation near tree parts]
         \label{correlation-near-tree-parts}
+        \leanok
+        \lean{TileStructure.Forest.correlation_near_tree_parts}
         \uses{tree-projection-estimate,dyadic-partition-2,bound-for-tree-projection}
         We have for all $\fu_1 \ne \fu_2 \in \fU$ with $\scI(\fu_1) \subset \scI(\fu_2)$ and all bounded $g_1, g_2$ with bounded support
         \begin{equation}
@@ -5067,7 +5079,7 @@ \section{Almost orthogonality of separated trees}
         \end{equation}
         \begin{equation}
             \label{eq-rhs-small-sep-tree}
-            \le 2^{222a^3} 2^{-Zn 2^{-10a}} \prod_{j =1}^2 \| S_{2, \fu_j} g_j\|_{L^2(\scI(\fu_1)}\,.
+            \le 2^{222a^3} 2^{-Zn 2^{-10a}} \prod_{j =1}^2 \| S_{2, \fu_j} g_j\|_{L^2(\scI(\fu_1))}\,.
         \end{equation}
     \end{lemma}
 
@@ -5075,6 +5087,8 @@ \section{Almost orthogonality of separated trees}
 
 \begin{lemma}[overlap implies distance]
     \label{overlap-implies-distance}
+    \leanok
+    \lean{TileStructure.Forest.𝔗_subset_𝔖₀, TileStructure.Forest.overlap_implies_distance}
     Let $\fu_1 \ne \fu_2 \in \fU$ with $\scI(\fu_1) \subset \scI(\fu_2)$. If $\fp \in \fT(\fu_1) \cup \fT(\fu_2)$ with $\scI(\fp) \cap \scI(\fu_1) \ne \emptyset$, then $\fp \in \mathfrak{S}$. In particular, we have $\fT(\fu_1) \subset \mathfrak{S}$.
 \end{lemma}
 
@@ -5113,6 +5127,8 @@ \subsection{A partition of unity}
 
     \begin{lemma}[dyadic partition 1]
         \label{dyadic-partition-1}
+        \leanok
+        \lean{TileStructure.Forest.union_𝓙₅, TileStructure.Forest.pairwiseDisjoint_𝓙₅}
         \uses{dyadic-partitions}
         We have that
         $$
@@ -5133,7 +5149,10 @@ \subsection{A partition of unity}
 
     \begin{lemma}[Lipschitz partition unity]
         \label{Lipschitz-partition-unity}
-           \uses{dyadic-partition-1,moderate-scale-change}
+        \leanok
+        \lean{TileStructure.Forest.sum_χ, TileStructure.Forest.χ_mem_Icc,
+          TileStructure.Forest.dist_χ_χ_le}
+        \uses{dyadic-partition-1,moderate-scale-change}
         There exists a family of functions $\chi_J$, $J \in \mathcal{J}'$ such that \begin{equation}
             \label{eq-pao-1}
             \mathbf{1}_{\scI(\fu_1)} = \sum_{J \in \mathcal{J}'} \chi_J\,,
@@ -5153,6 +5172,8 @@ \subsection{A partition of unity}
 
     \begin{lemma}[moderate scale change]
         \label{moderate-scale-change}
+        \leanok
+        \lean{TileStructure.Forest.moderate_scale_change}
 
         If $J, J' \in \mathcal{J'}$ with
         $$
@@ -5250,6 +5271,8 @@ \subsection{H\"older estimates for adjoint tree operators}
 
     \begin{lemma}[Holder correlation tree]
         \label{Holder-correlation-tree}
+        \leanok
+        \lean{TileStructure.Forest.holder_correlation_tree}
         \uses{global-tree-control-2}
         We have for all $J \in \mathcal{J}'$ that
         \begin{equation}
@@ -5263,6 +5286,8 @@ \subsection{H\"older estimates for adjoint tree operators}
     We begin with the following H\"older continuity estimate for adjoints of operators associated to tiles.
     \begin{lemma}[Holder correlation tile]
         \label{Holder-correlation-tile}
+        \leanok
+        \lean{TileStructure.Forest.holder_correlation_tile}
         \uses{adjoint-tile-support}
         Let $\fu \in \fU$ and $\fp \in \fT(\fu)$. Then for all $y, y' \in X$ and all bounded $g$ with bounded support, we have
         $$
@@ -5385,8 +5410,10 @@ \subsection{H\"older estimates for adjoint tree operators}
 
     \begin{lemma}[limited scale impact]
         \label{limited-scale-impact}
+        \leanok
+        \lean{TileStructure.Forest.limited_scale_impact}
         \uses{overlap-implies-distance}
-        Let $\fp \in \fT_2 \setminus \mathfrak{S}$, $J \in \mathcal{J}'$ and suppose that
+        Let $\fp \in \fT(\fu_2) \setminus \mathfrak{S}$, $J \in \mathcal{J}'$ and suppose that
         $$
            B(\scI(\fp)) \cap B^\circ(J) \ne \emptyset\,.
         $$
@@ -5433,6 +5460,8 @@ \subsection{H\"older estimates for adjoint tree operators}
 
     \begin{lemma}[local tree control]
         \label{local-tree-control}
+        \leanok
+        \lean{TileStructure.Forest.local_tree_control}
         \uses{limited-scale-impact}
         For all $J \in \mathcal{J}'$ and all bounded $g$ with bounded support
         $$
@@ -5475,6 +5504,8 @@ \subsection{H\"older estimates for adjoint tree operators}
 
     \begin{lemma}[scales impacting interval]
         \label{scales-impacting-interval}
+        \leanok
+        \lean{TileStructure.Forest.scales_impacting_interval}
         \uses{overlap-implies-distance}
         Let $\fC = \fT(\fu_1)$ or $\fC = \fT(\fu_2) \cap \mathfrak{S}$. Then for each $J \in \mathcal{J}'$ and $\fp \in \fC$ with $B(\scI(\fp)) \cap B(J) \neq \emptyset$, we have $\ps(\fp) \ge s(J)$.
     \end{lemma}
@@ -5485,6 +5516,8 @@ \subsection{H\"older estimates for adjoint tree operators}
 
     \begin{lemma}[global tree control 1]
         \label{global-tree-control-1}
+        \leanok
+        \lean{TileStructure.Forest.global_tree_control1_1, TileStructure.Forest.global_tree_control1_2}
         \uses{Holder-correlation-tile,scales-impacting-interval}
         Let $\fC = \fT(\fu_1)$ or $\fC = \fT(\fu_2) \cap \mathfrak{S}$. Then for each $J \in \mathcal{J}'$ and all bounded $g$ with bounded support, we have
         \begin{align}
@@ -5536,10 +5569,12 @@ \subsection{H\"older estimates for adjoint tree operators}
 
     \begin{lemma}[global tree control 2]
         \label{global-tree-control-2}
+        \leanok
+        \lean{TileStructure.Forest.global_tree_control2}
         \uses{global-tree-control-1, local-tree-control}
         We have for all $J \in \mathcal{J}'$ and all bounded $g$ with bounded support
         $$
-            \sup_{B(J)} |T^*_{\mathfrak{T}_2 \cap \mathfrak{S}} g| \le \inf_{B^\circ{}(J)} |T^*_{\mathfrak{T}_2} g| + 2^{155a^3} \inf_{J} M_{\mathcal{B},1}|g|\,.
+            \sup_{B(J)} |T^*_{\fT(\fu_2) \cap \mathfrak{S}} g| \le \inf_{B^\circ{}(J)} |T^*_{\fT(\fu_2)} g| + 2^{155a^3} \inf_{J} M_{\mathcal{B},1}|g|\,.
         $$
     \end{lemma}
 
@@ -5603,6 +5638,8 @@ \subsection{The van der Corput estimate}
 \label{subsubsec-van-der-corput}
     \begin{lemma}[lower oscillation bound]
         \label{lower-oscillation-bound}
+        \leanok
+        \lean{TileStructure.Forest.lower_oscillation_bound}
         \uses{overlap-implies-distance}
         For all $J \in \mathcal{J}'$, we have that
         $$
@@ -5677,6 +5714,8 @@ \section{Proof of The Remaining Tiles Lemma}
     note that this is different from the $\mathcal{J}'$ defined in the previous subsection.
     \begin{lemma}[dyadic partition 2]
         \label{dyadic-partition-2}
+        \leanok
+        \lean{TileStructure.Forest.union_𝓙₆, TileStructure.Forest.pairwiseDisjoint_𝓙₆}
         \uses{dyadic-partitions}
         We have
         $$
@@ -5692,10 +5731,12 @@ \section{Proof of The Remaining Tiles Lemma}
 
     \begin{lemma}[bound for tree projection]
         \label{bound-for-tree-projection}
+        \leanok
+        \lean{TileStructure.Forest.bound_for_tree_projection}
         \uses{adjoint-tile-support,overlap-implies-distance,dyadic-partition-2,thin-scale-impact,square-function-count}
         We have
         $$
-            \|P_{\mathcal{J}'}|T_{\mathfrak{T}_2 \setminus \mathfrak{S}}^* g_2|\|_2
+            \|P_{\mathcal{J}'}|T_{\fT(\fu_2) \setminus \mathfrak{S}}^* g_2|\|_2
             \le 2^{118a^3} 2^{-\frac{100}{202a}Zn\kappa} \|\mathbf{1}_{\scI(\fu_1)} M_{\mathcal{B},1} |g_2|\|_2
         $$
     \end{lemma}
@@ -5723,7 +5764,9 @@ \section{Proof of The Remaining Tiles Lemma}
 
     \begin{lemma}[thin scale impact]
         \label{thin-scale-impact}
-        If $\fp \in \fT_2 \setminus \mathfrak{S}$ and $J \in \mathcal{J'}$ with $B(\scI(\fp)) \cap B(J) \ne \emptyset$, then
+        % \leanok
+        % \lean{TileStructure.Forest.thin_scale_impact}
+        If $\fp \in \fT(\fu_2) \setminus \mathfrak{S}$ and $J \in \mathcal{J'}$ with $B(\scI(\fp)) \cap B(J) \ne \emptyset$, then
         $$
             \ps(\fp) \le s(J) + 2 - \frac{Zn}{202a^3}\,.
         $$
@@ -5771,6 +5814,8 @@ \section{Proof of The Remaining Tiles Lemma}
 
     \begin{lemma}[square function count]
         \label{square-function-count}
+        \leanok
+        \lean{TileStructure.Forest.square_function_count}
         For each $J \in \mathcal{J}'$, we have
         $$
             \frac{1}{\mu(J)} \int_J \Bigg(\sum_{\substack{I \in \mathcal{D}, s(I) = s(J) - s\\ I \cap \scI(\fu_1) = \emptyset\\
@@ -5778,8 +5823,7 @@ \section{Proof of The Remaining Tiles Lemma}
         $$
     \end{lemma}
 
-    \begin{proof}[Proof of \Cref{square-function-count}]
-        \proves{square-function-count}
+    \begin{proof}
         Since $J \in \mathcal{J}'$ we have $J \subset \scI(\fu_1)$. Thus, if $B(I) \cap J \ne \emptyset$ then
     \begin{equation}
         \label{eq-sep-small-incl}
@@ -5808,7 +5852,7 @@ \section{Proof of The Remaining Tiles Lemma}
     \proves{bound-for-tree-projection}
     Expanding the definition of $P_{\mathcal{J}'}$, we have
     $$
-        \|P_{\mathcal{J}'}|T_{\mathfrak{T}_2 \setminus \mathfrak{S}}^* g_2|\|_2
+        \|P_{\mathcal{J}'}|T_{\fT(\fu_2) \setminus \mathfrak{S}}^* g_2|\|_2
     $$
     $$
         = \left(\sum_{J \in \mathcal{J}'} \frac{1}{\mu(J)} \left|\int_J \sum_{\fp \in \fT(\fu_2) \setminus \mathfrak{S}} T_{\fp}^* g_2 \, \mathrm{d}\mu(y) \right|^2 \right)^{1/2}\,.
@@ -5902,6 +5946,9 @@ \section{Forests}
 
 \begin{lemma}[forest row decomposition]
     \label{forest-row-decomposition}
+    \leanok
+    \lean{TileStructure.Forest.rowDecomp, TileStructure.Forest.biUnion_rowDecomp,
+    TileStructure.Forest.pairwiseDisjoint_rowDecomp}
     Let $(\fU, \fT)$ be an $n$-forest. Then there exists a decomposition
     $$
         \fU = \dot{\bigcup_{1 \le j \le 2^n}} \fU_j
@@ -5927,6 +5974,8 @@ \section{Forests}
 
 \begin{lemma}[row bound]
     \label{row-bound}
+    \leanok
+    \lean{TileStructure.Forest.row_bound, TileStructure.Forest.indicator_row_bound}
     \uses{densities-tree-bound,adjoint-tile-support}
     For each $1 \le j \le 2^n$ and each bounded $g$ with bounded support, we have
     \begin{equation}
@@ -5973,6 +6022,8 @@ \section{Forests}
 
 \begin{lemma}[row correlation]
     \label{row-correlation}
+    \leanok
+    \lean{TileStructure.Forest.row_correlation}
     \uses{adjoint-tree-control,correlation-separated-trees}
     For all $1 \le j < j' \le 2^n$ and for all bounded $g_1, g_2$ with bounded support, it holds that
     $$
@@ -6030,6 +6081,8 @@ \section{Forests}
 
 \begin{lemma}[disjoint row support]
     \label{disjoint-row-support}
+    \leanok
+    \lean{TileStructure.Forest.pairwiseDisjoint_rowSupport}
     The sets $E_j$, $1 \le j \le 2^n$ are pairwise disjoint.
 \end{lemma}
 
@@ -6110,6 +6163,8 @@ \chapter{Proof of the H\"older cancellative condition}
 
 \begin{lemma}[Lipschitz Holder approximation]
     \label{Lipschitz-Holder-approximation}
+    % \leanok
+    % \lean{TileStructure.Forest.}
     \leanok
     \lean{support_holderApprox_subset, dist_holderApprox_le, lipschitzWith_holderApprox}
     Let $z\in X$ and $R>0$. Let $\varphi: X \to \mathbb{C}$ be a function supported in the ball
@@ -7715,8 +7770,6 @@ \section{Calder\'on-Zygmund Decomposition}
 
 \chapter{Proof of The Classical Carleson Theorem}
 
-
-
 The convergence of partial Fourier sums is proved in
 \Cref{10classical} in two steps. In the first step,
 we establish convergence on a suitable dense subclass of functions. We choose smooth functions as subclass, the convergence is stated in \Cref{convergence-for-smooth} and proved in \Cref{10smooth}.
@@ -7810,9 +7863,20 @@ \section{The classical Carleson theorem}
     \end{equation}
 \end{lemma}
 
-We are now ready to prove classical Carleson:
-\begin{proof} [Proof of \Cref{classical-Carleson}]
-\proves{classical-Carleson}
+We are now ready to prove \Cref{classical-carleson}. We first prove a version with explicit exceptional sets.
+
+\begin{theorem}[classical Carleson with exceptional sets]
+    \label{exceptional-set-carleson}
+    \leanok
+    \lean{exceptional_set_carleson}
+    \uses{smooth-approximation, convergence-for-smooth,
+    control-approximation-effect}
+    Let $f$ be a $2\pi$-periodic complex-valued continuous function on $\mathbb{R}$. For all $\epsilon>0$, there exists a Borel set $E\subset [0,2\pi]$ with Lebesgue measure $|E|\le \epsilon$ and a positive integer $N_0$ such that for all $x\in [0,2\pi]\setminus E$ and all integers $N>N_0$, we have
+    \begin{equation}\label{aeconv}
+    |f(x)-S_N f(x)|\le \epsilon.
+    \end{equation}
+\end{theorem}
+\begin{proof}
 \leanok
 Let $N_0$ be as in \Cref{convergence-for-smooth}.
 For every
@@ -7833,6 +7897,18 @@ \section{The classical Carleson theorem}
 This shows \eqref{aeconv} for the given $E$ and $N_0$.
 \end{proof}
 
+Now we turn to the proof of the statement of Carleson theorem given in the introduction.
+\begin{proof}[Proof of \Cref{classical-carleson}]
+\proves{classical-carleson}
+\leanok
+%Note that mere continuity implies uniform continuity in the setting of this theorem.
+By applying \Cref{exceptional-set-carleson} with a sequence of $\epsilon_n:= 2^{-n}\delta$ for $n\ge 1$ and taking the union
+of corresponding exceptional sets $E_n$, we see that outside a set of measure $\delta$, the partial Fourier
+sums converge pointwise for $N\to \infty$. Applying this with a sequence of $\delta$ shrinking to zero and
+taking the intersection of the corresponding exceptional sets, which has measure zero, we see that the Fourier
+series converges outside a set of measure zero.
+\end{proof}
+
 Let $\kappa:\R\to \C$ be the function defined by
 $\kappa(0)=0$ and for $0<|x|<1$
 \begin{equation}\label{eq-hilker}