1: \begin{abstract}

2:   We prove a new generalization of a theorem of Carleson, namely bounds for a generalized Carleson operator on doubling metric measure spaces. 

3:   Additionally, we explicitly reduce Carleson's classical result on pointwise convergence of Fourier series to this new theorem. 

4:   Both proofs are presented in great detail, suitable as a blueprint for computer verification using the current capabilities of the software package Lean. 

5: Note  that even Carleson's classical result has not yet been computer-verified.

6: \end{abstract}

7: