A finitary Kronecker's lemma and large deviations in the Strong Law of Large numbers on Banach spaces

TL;DR

This paper develops a finitary version of Kronecker's lemma using proof mining, providing uniform rates for the Strong Law of Large Numbers in Banach spaces and analyzing the computational limitations and implications of the lemma.

Contribution

It introduces a finitary variant of Kronecker's lemma, explores its computational content, and connects it to quantitative results in probability theory within Banach spaces.

Findings

Finitary Kronecker's lemma yields uniform convergence rates in Banach spaces.

Demonstrates the ineffectiveness of Kronecker's lemma in computability terms.

Shows how the lemma's limitations affect the Strong Law of Large Numbers.

Abstract

We explore the computational content of Kronecker's lemma via the proof-theoretic perspective of proof mining and utilise the resulting finitary variant of this fundamental result to provide new rates for the Strong Law of Large Numbers for random variables taking values in type $p$ Banach spaces, which in particular are very uniform in the sense that they do not depend on the distribution of the random variables. Furthermore, we provide computability-theoretic arguments to demonstrate the ineffectiveness of Kronecker's lemma and investigate the result from the perspective of Reverse Mathematics. In addition, we demonstrate how this ineffectiveness from Kronecker's lemma trickles down to the Strong Law of Large Numbers by providing a construction that shows that computable rates of convergence are not always possible. Lastly, we demonstrate how Kronecker's lemma falls under a class of deterministic formulas whose solution to their Dialectica interpretation satisfies a continuity property and how, for such formulas, one obtains an upgrade principle that allows one to lift computational interpretations of deterministic results to quantitative results for their probabilistic analogue. This result generalises the previous work of the author and Pischke.