  We prove a new generalization of a theorem of Carleson, namely bounds for a
generalized Carleson operator on doubling metric measure spaces. Additionally,
we explicitly reduce Carleson's classical result on pointwise convergence of
Fourier series to this new theorem. Both proofs are presented in great detail,
suitable as a blueprint for computer verification using the current
capabilities of the software package Lean. Note that even Carleson's classical
result has not yet been computer-verified.
