## Abstract

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.

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.

Original language | English |
---|---|

Article number | 103231 |

Number of pages | 30 |

Journal | Annals of Pure and Applied Logic |

Volume | 174 |

Issue number | 4 |

Early online date | 13 Dec 2022 |

DOIs | |

Publication status | E-pub ahead of print - 13 Dec 2022 |