Contents

1. 1. Formalization of Carleson's theorem
   1. 1.1. Introduction
      1. 1.1.1. Statement of the metric space Carleson theorems
   2. 1.2. Proof of Metric Space Carleson, overview
      1. 1.2.1. Auxiliary lemmas
   3. 1.3. Proof of Metric Space Carleson
   4. 1.4. Proof of Finitary Carleson
      1. 1.4.1. Proof of Grid Existence Lemma
      2. 1.4.2. Proof of Tile Structure Lemma
   5. 1.5. Proof of discrete Carleson
      1. 1.5.1. Organisation of the tiles
      2. 1.5.2. Proof of the Exceptional Sets Lemma
      3. 1.5.3. Auxiliary lemmas
      4. 1.5.4. Proof of the Forest Union Lemma
      5. 1.5.5. Proof of the Forest Complement Lemma
   6. 1.6. Proof of the Antichain Operator Proposition
      1. 1.6.1. The density arguments
      2. 1.6.2. Proof of the Tile Correlation Lemma
      3. 1.6.3. Proof of the Antichain Tile Count Lemma
   7. 1.7. Proof of the Forest Operator Proposition
      1. 1.7.1. The pointwise tree estimate
      2. 1.7.2. An auxiliary L^2 tree estimate
      3. 1.7.3. The quantitative L^2 tree estimate
      4. 1.7.4. Almost orthogonality of separated trees
      5. 1.7.5. Proof of the Tiles with large separation Lemma
         1. 1.7.5.1. A partition of unity
         2. 1.7.5.2. Holder estimates for adjoint tree operators
         3. 1.7.5.3. The van der Corput estimate
      6. 1.7.6. Proof of The Remaining Tiles Lemma
      7. 1.7.7. Forests
   8. 1.8. Proof of the H"older cancellative condition
   9. 1.9. Proof of Vitali covering and Hardy--Littlewood
   10. 1.10. Two-sided Metric Space Carleson
   11. 1.11. Proof of The Classical Carleson Theorem
       1. 1.11.1. The classical Carleson theorem
       2. 1.11.2. Smooth functions
       3. 1.11.3. The truncated Hilbert transform
       4. 1.11.4. The proof of the van der Corput Lemma
       5. 1.11.5. Partial sums as orthogonal projections
       6. 1.11.6. Difference control
       7. 1.11.7. Carleson on the real line
2. Dependency Graph
3. Blueprint Summary