Effective weak convergence and tightness of measures in computable Polish spaces

TL;DR

This paper develops an effective version of Prokhorov's Theorem for computable Polish spaces, linking tightness and weak convergence of measures in a constructive framework.

Contribution

It generalizes effective weak convergence notions to computable Polish spaces and proves an effective Prokhorov's Theorem, bridging classical probability and computability theory.

Findings

Established an effective notion of tightness for measures on computable Polish spaces.

Proved an effective version of Prokhorov's Theorem for computable sequences.

Extended previous real-line results to general computable Polish spaces.

Abstract

Prokhorov's Theorem in probability theory states that a family $\Gamma$ of probability measures on a Polish space is tight if and only if every sequence in $\Gamma$ has a weakly convergent subsequence. Due to the highly non-constructive nature of (relative) sequential compactness, however, the effective content of this theorem has not been studied. To this end, we generalize the effective notions of weak convergence of measures on the real line due to McNicholl and Rojas to computable Polish spaces. Then, we introduce an effective notion of tightness for families of measures on computable Polish spaces. Finally, we prove an effective version of Prokhorov's Theorem for computable sequences of probability measures.