A finitization of Littlewood’s Tauberian theorem and an application in Tauberian remainder theory

We analyse Littlewood’s 1911 Tauberian theorem from a proof theo-
retic perspective. We first use Goedel’s Dialectica interpretation to give a
computational interpretation the theorem, producing a finitary formula-
tion of the result and, with the help of known quantitative results from
approximation theory, extracting concrete bounds from the proof. Our fini-
tary Tauberian theorem can be given an intuitive game semantics, with the
bounds corresponding to a winning strategy. We then use our finitization
to produce two general remainder theorems in terms of rates of conver-
gence and metastability. We rederive the traditional remainder estimate for
Littlewood’s theorem as a special case of these.