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.5.6. Proof of the Antichain Operator Proposition
      7. 1.5.7. The density arguments
      8. 1.5.8. Proof of the Tile Correlation Lemma
      9. 1.5.9. Proof of the Antichain Tile Count Lemma
      10. 1.5.10. Proof of the Forest Operator Proposition
      11. 1.5.11. The pointwise tree estimate
      12. 1.5.12. An auxiliary L^2 tree estimate
      13. 1.5.13. The quantitative L^2 tree estimate
      14. 1.5.14. Almost orthogonality of separated trees
      15. 1.5.15. Proof of the Tiles with large separation Lemma
          1. 1.5.15.1. A partition of unity
          2. 1.5.15.2. Holder estimates for adjoint tree operators
          3. 1.5.15.3. The van der Corput estimate
      16. 1.5.16. Proof of The Remaining Tiles Lemma
      17. 1.5.17. Forests
      18. 1.5.18. Proof of the H"older cancellative condition
      19. 1.5.19. Proof of Vitali covering and Hardy--Littlewood
2. Dependency Graph
3. Blueprint Summary