Probability sequences on compact metric spaces have integral-convergent subsequences

Fix the dense family $(f_j)$ of [F1]. Continuous real functions on $K$ are bounded, as proved there; they are Borel measurable by continuity. For every Borel probability $\nu$, [F4] bounds the integral of $\mathrm{\mid }f\mathrm{\mid }$ by $\mathrm{\parallel }f{\mathrm{\parallel }}_{\mathrm{\infty }}$, so $f$ is integrable. Positivity and [F5], applied to $\mathrm{\parallel }f-g{\mathrm{\parallel }}_{\mathrm{\infty }}\pm (f-g)$, give $\mathrm{\mid }\int fd\nu -\int gd\nu \mathrm{\mid }\le \mathrm{\parallel }f-g{\mathrm{\parallel }}_{\mathrm{\infty }}$. In particular $a_{n,j}=\int f_{j}d{\mu }_n$ is a bounded real sequence for each $j$.

There is a deterministic convergent-subsequence rule for a bounded real sequence $(a_n)$ restricted to an infinite subset $S$ of the positive integers, with a specified bound $M\ge 0$. Start with $I_0=[-M,M]$. Bisect the current closed interval; retain its left half if infinitely many indices in $S$ have values there, and otherwise retain the right half, which must have infinitely many such indices. At stage $m\ge 1$ choose the least eligible index $k_m\in S$ greater than $k_{m-1}$, with $k_0=0$, whose value lies in $I_m$. The indices exist because an infinite subset of the naturals is unbounded. The intervals are nested and have lengths $2M{2}^{-m}$, so the selected values are Cauchy. They converge: [F2] provides a convergent subsequence with limit $L$, and the Cauchy estimate followed by the triangle inequality with a sufficiently late member of that subsequence gives $\mathrm{\mid }{a}_{k_m}-L\mathrm{\mid }<\epsilon$ for all sufficiently large $m$. This also works for $M=0$. Left-half precedence and least indices make every stage unique, so ordinary recursion suffices; no Dependent Choice is used.

Set $S_0={\mathbb{N}}_{>0}$. Recursively apply the rule of step 1.2 to coordinate $a_{n,j}$ on $S_{j-1}$ with $M=\mathrm{\parallel }{f}_j{\mathrm{\parallel }}_{\mathrm{\infty }}$, and let $S_j$ be its infinite output index set. Thus $S_j\subseteq S_{j-1}$, and the $j$th coordinate converges along the increasing enumeration of $S_j$. Let $n_r$ be the $r$th smallest member of $S_r$. Since $S_{r+1}\subseteq S_r$, its $(r+1)$th member is at least the $(r+1)$th member of $S_r$, which exceeds $n_r$. Thus $(n_r)$ is strictly increasing. For every fixed $j$, all $n_r$ with $r\ge j$ belong to $S_j$ and increase without bound, so $\int f_{j}d{\mu }_{n_r}$ converges. All index sets and enumerations are defined uniquely by the fixed rule.

For $f\in C(K,\mathbb{R})$ and $\epsilon >0$, choose one $j$ with $\mathrm{\parallel }f-f_j{\mathrm{\parallel }}_{\mathrm{\infty }}<\epsilon \mathrm{/}3$. For large $r,s$, step 2.1 gives $\mathrm{\mid }\int f_{j}d{\mu }_{n_r}-\int f_{j}d{\mu }_{n_s}\mathrm{\mid }<\epsilon \mathrm{/}3$; the two uniform error bounds of step 1.1 show that $(\int fd{\mu }_{n_r}{)}_r$ is Cauchy. It is bounded, and hence converges by the Cauchy-plus-[F2] argument in step 1.2. Define $\mathrm{\Lambda }(f)$ to be this unique limit. Passing to limits in [F5] proves real linearity, positivity passes to limits of nonnegative real numbers, and $\mathrm{\Lambda }(1)=1$ since every ${\mu }_{n_r}$ is a probability. Apply [F3] with exactly these hypotheses to obtain the regular Borel probability $\mu$ and the asserted convergence for every $f$. The choices used are those in [F1] and [F3], both explicitly bounded by countable choice; neither the nested extraction nor the definition of the unique limit selects an arbitrary family of witnesses.