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 |