Kit for def:weak-convergence-measures-metric

In the setting of Measurable Functions and the Lebesgue Integral: Standing Notation and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $q\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{q-1}$ be distinct set variables, and let $i,j,k,l<q$, not necessarily distinct. Let $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$ and $1$ be the ten parameters of Kit for def:measure-measure-space, other than $x_{0},\dots,x_{q-1}$, with the kinds and values given there, and let $\mathbb{R}$, $\le$, $<$, $+$, $\cdot$, $d_{\mathbb{R}}$, $\iota$ and $\mathcal{B}(\mathbb{R})$ be further distinct class variables whose values are the set $\mathbb{R}$ of real numbers, its order, its strict order, its addition and multiplication, the distance on $\mathbb{R}$, the identity on $\mathbb{R}$ and the Borel $\sigma$-algebra of $\mathbb{R}$. The parameters of the following results are these variables, each with the kind given here. The parameters $\mathbb{R}$, $\le$, $<$, $+$, $0$ and $\mathbb{N}$ of Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (i) and Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites (v), the parameters $\mathbb{R}$, $+$, $0$ and $\le$ of Kit for def:continuous-map-metric-spaces (iv), the parameters $\mathbb{R}$, $\le$, $<$, $+$, $\cdot$, $0$ and $1$ of Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (iii), and the parameters $\mathbb{N}$, $\mathbb{R}$, $\le$, $<$ and $0$ of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) for the metric space $(\mathbb{R},d_{\mathbb{R}})$ are the variables of the same names, and the parameters $X$ and $d$ of the last are $\mathbb{R}$ and $d_{\mathbb{R}}$. Of the parameters of The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (iii) for $X=\mathbb{R}$ and $\mathcal{F}=\mathcal{B}(\mathbb{R})$, its $X$ and $\mathcal{F}$ are $\mathbb{R}$ and $\mathcal{B}(\mathbb{R})$; its $[-\infty,\infty]$, the order of $[-\infty,\infty]$, $[0,\infty]$ and the sum on $[0,\infty]$ are $E$, $L$, $Z$ and $P$; its $\mathbb{R}$, $\le$, $<$, $+$, $\cdot$, $0$ and $1$ of the real numbers are the variables of the same names; and its other parameters are further distinct class variables, other than all the above, with their values there. A condition on $x_{0},\dots,x_{q-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{q-1}$ in place of the set variables listed in Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and as parameters the eighteen variables above together with these further variables. Metric spaces are as in Metric Space (vi), sequences as in Sequences (i), the Borel $\sigma$-algebra $\mathcal{B}(S)$ of a metric space $(S,d)$ as in Borel Sigma-Algebra of a Metric Space (i), finite measures as in Measure, Measure Space, and Probability Measure (iii), and weak convergence $\mu_{n}\Rightarrow\mu$ as in Weak Convergence of Finite Borel Measures on a Metric Space (i).

(i) Weak convergence. With $S=x_{i}$, $d=x_{j}$, $(\mu_{n})=x_{k}$ and $\mu=x_{l}$, the condition "$(S,d)$ is a metric space, $(\mu_{n})$ is a sequence of finite measures on $(S,\mathcal{B}(S))$, $\mu$ is a finite measure on $(S,\mathcal{B}(S))$, and $\mu_{n}\Rightarrow\mu$" on $x_{0},\dots,x_{q-1}$ is predicative.

(ii) The set of measures to which a sequence converges weakly. For every metric space $(S,d)$ and every sequence $(\mu_{n})$ of finite measures on $(S,\mathcal{B}(S))$ there is a class $C$ such that, for every class $\mu$, $\mu\in C$ if and only if $\mu$ is a finite measure on $(S,\mathcal{B}(S))$ and $\mu_{n}\Rightarrow\mu$; and $C$ is a set.

(iii) The set of sequences converging weakly to a measure. For every metric space $(S,d)$ and every finite measure $\mu$ on $(S,\mathcal{B}(S))$ there is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is a sequence $(a_{n})$ of finite measures on $(S,\mathcal{B}(S))$ with $a_{n}\Rightarrow\mu$; and $C$ is a set.