Proof of Kit for def:convergence-in-distribution-metric

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, and routine facts about maps and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (v), Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and so is the agreement of the earlier version of sequences read by published results cited below with its current version (The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i)). The given $x_{0},\dots,x_{q-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{9}$ are distinct also when $q<10$. The letters $S$, $d$, $\Omega_{\bullet}$, $\mathcal{F}_{\bullet}$, $P_{\bullet}$, $X_{\bullet}$, $\Omega$, $\mathcal{F}$, $P$ and $X$ denote $x_{0},\dots,x_{9}$, where $\Omega_{\bullet}$, $\mathcal{F}_{\bullet}$, $P_{\bullet}$ and $X_{\bullet}$ stand for $(\Omega_{n})$, $(\mathcal{F}_{n})$, $(P_{n})$ and $(X_{n})$; every other letter used below as a variable denotes one of $x_{10},x_{11},\dots$, distinct letters denoting distinct variables, and a formula taken from another item is used at the variables named by Renaming and Substituting Variables in Predicative Formulas (i), its bound variables, like those of every formula taken from another result, renamed where necessary so that none is captured and none is a parameter. The value of the parameter $\mathbb{N}$ is the set $\mathbb{N}$ of Sums of Sequences in [0,∞] as Typed Terms and as a Map (i), the set of natural numbers, from which sequences are maps (Sequences (i)).

Random elements. By Kit for def:probability-space-random-variable (iv), with its $N$ equal to $6$, its indices $i,j,k,l,m,p$ equal to $0,\dots,5$ and its seventeen parameters those of the statement, which have the values and kinds that kit prescribes, and by renaming, there is a predicative formula $\rho(o,f,p,S,d,e)$ that holds if and only if $(o,f)$ is a measurable space, $p$ is a measure on it, $(o,f,p)$ is a probability space, $d:S\times S\to\mathbb{R}$ is a map, $(S,d)$ is a metric space and $e$ is a random element of $S$ on $(o,f,p)$. The first two parts follow from the third (Probability Spaces, Events and Random Elements (i), Measure, Measure Space, and Probability Measure (ii)) and the fourth from the fifth (Metric Space (vi)); so $\rho(o,f,p,S,d,e)$ holds if and only if $(o,f,p)$ is a probability space, $(S,d)$ is a metric space and $e$ is a random element of $S$ on $(o,f,p)$.

Weak convergence. By Kit for def:weak-convergence-measures-metric (i), with its $q$ equal to $4$ and its $i,j,k,l$ equal to $0,1,2,3$, and by renaming, there is a predicative formula $W(S,d,s,\mu)$, with parameters among those of the statement, that holds if and only if $(S,d)$ is a metric space, $s$ is a sequence of finite measures on $(S,\mathcal{B}(S))$, $\mu$ is a finite measure on $(S,\mathcal{B}(S))$ and $s\Rightarrow\mu$, where $\mathcal{B}(S)$ is the Borel $\sigma$-algebra of $(S,d)$.

Laws. Let

$$\ell(p,e,m)=\forall B\,\forall v\,\Bigl((B,v)\in m\Rightarrow\exists w\,\bigl(\forall u\,(u\in w\Leftrightarrow\exists y\,(y\in B\wedge(u,y)\in e))\wedge(w,v)\in p\bigr)\Bigr).$$

It is predicative (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii)). Claim: let $(o,f,p)$ be a probability space, $(S,d)$ a metric space, $e$ a random element of $S$ on $(o,f,p)$ with law $p_{e}$, and $m$ a finite measure on $(S,\mathcal{B}(S))$. Then $p_{e}$ is a finite measure on $(S,\mathcal{B}(S))$, and $\ell(p,e,m)$ holds if and only if $m=p_{e}$. Indeed, $p_{e}$ is a probability measure on $(S,\mathcal{B}(S))$ (The Law of a Random Element (i)), so $p_{e}(S)=1<\infty$, as $1$ is real (Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii)), and $p_{e}$ is finite (Measure, Measure Space, and Probability Measure (v), Measure, Measure Space, and Probability Measure (iii)). As $m$ is a map $m:\mathcal{B}(S)\to[0,\infty]$ (Measure, Measure Space, and Probability Measure (i)), the sets $B$ and $v$ with $(B,v)\in m$ are the $B\in\mathcal{B}(S)$ with $v=m(B)$. Let $B\in\mathcal{B}(S)$. As $e:o\to S$ is $f/\mathcal{B}(S)$-measurable (Probability Spaces, Events and Random Elements (iii)), its preimage $e^{-1}(B)$ belongs to $f$ (Measurable Map, and the Set of Measurable Maps (i); in particular it is a set). For a set $u$, $\exists y\,(y\in B\wedge(u,y)\in e)$ holds if and only if $u\in o$ and $e(u)\in B$, that is, if and only if $u\in e^{-1}(B)$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ix)); so, by the axiom of extensionality, the only set $w$ satisfying the first conjunct after $\exists w$ is $e^{-1}(B)$, and as $p:f\to[0,\infty]$ is a map, $(e^{-1}(B),v)\in p$ holds if and only if $v=p(e^{-1}(B))$. Hence $\ell(p,e,m)$ holds if and only if

$$m(B)=p\bigl(e^{-1}(B)\bigr)=p_{e}(B)\qquad(B\in\mathcal{B}(S)),$$

the second equality being The Law of a Random Element (i). As $m$ and $p_{e}$ are maps $\mathcal{B}(S)\to[0,\infty]$, this holds if and only if $m=p_{e}$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)). This proves the claim.

The formula for convergence in distribution. Let $\Phi$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vi), and for a variable $G$ let

$$\psi(G)=\Phi(G)\wedge\forall n\,\bigl(n\in\mathbb{N}\Leftrightarrow\exists z\,((n,z)\in G)\bigr),$$

which holds if and only if $G$ is a function with domain $\mathbb{N}$ (Relations, Domain, Range, Inverse and Composition (ii)). Let

$$\begin{aligned} \tau={}&\forall n\,\forall o\,\forall f\,\forall p\,\forall e\,\bigl((n\in\mathbb{N}\wedge(n,o)\in\Omega_{\bullet}\wedge(n,f)\in\mathcal{F}_{\bullet}\wedge(n,p)\in P_{\bullet}\wedge(n,e)\in X_{\bullet})\Rightarrow\rho(o,f,p,S,d,e)\bigr),\\ \gamma={}&\exists s\,\exists\mu\,\Bigl(W(S,d,s,\mu)\wedge\ell(P,X,\mu)\wedge\forall n\,\forall m\,\forall p\,\forall e\,\bigl((n\in\mathbb{N}\wedge(n,m)\in s\wedge(n,p)\in P_{\bullet}\wedge(n,e)\in X_{\bullet})\Rightarrow\ell(p,e,m)\bigr)\Bigr),\\ \alpha={}&\psi(\Omega_{\bullet})\wedge\psi(\mathcal{F}_{\bullet})\wedge\psi(P_{\bullet})\wedge\psi(X_{\bullet})\wedge\tau\wedge\rho(\Omega,\mathcal{F},P,S,d,X)\wedge\gamma. \end{aligned}$$

These are predicative (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii)), every quantifier added being over a set variable, and the free variables of $\alpha$ are among $x_{0},\dots,x_{9}$ and the parameters.

Let sets $S$, $d$, $\Omega_{\bullet}$, $\mathcal{F}_{\bullet}$, $P_{\bullet}$, $X_{\bullet}$, $\Omega$, $\mathcal{F}$, $P$ and $X$ be assigned to $x_{0},\dots,x_{9}$. The first four conjuncts of $\alpha$ hold exactly when $\Omega_{\bullet}$, $\mathcal{F}_{\bullet}$, $P_{\bullet}$ and $X_{\bullet}$ are functions with domain $\mathbb{N}$; then, for $n\in\mathbb{N}$, the only sets $o$, $f$, $p$ and $e$ with $(n,o)\in\Omega_{\bullet}$, $(n,f)\in\mathcal{F}_{\bullet}$, $(n,p)\in P_{\bullet}$ and $(n,e)\in X_{\bullet}$ are the values $\Omega_{n}$, $\mathcal{F}_{n}$, $P_{n}$ and $X_{n}$. So, by the paragraph on random elements, the first six conjuncts of $\alpha$ together hold exactly when every part of the condition of (i) other than convergence in distribution holds. If they fail, then $\alpha$ fails together with that condition. Let them hold, and write $P_{X_{n}}$ for the law of $X_{n}$ on $(\Omega_{n},\mathcal{F}_{n},P_{n})$ and $P_{X}$ for that of $X$ on $(\Omega,\mathcal{F},P)$ (The Law of a Random Element (i), with the notation of Probability Spaces: Notation (ii)).

As $P_{X}$ is a probability measure on $(S,\mathcal{B}(S))$ (The Law of a Random Element (i)), $(S,\mathcal{B}(S))$ is a measurable space, and by Kit for def:measure-measure-space (x) the finite measures on it form a set $\mathcal{M}_{\mathrm{fin}}$. By the claim, $P_{X}$ and each $P_{X_{n}}$ belong to $\mathcal{M}_{\mathrm{fin}}$, and Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathcal{M}_{\mathrm{fin}}$ as its $a$ and $b$ (the expression $t$ there being $t(n)=P_{X_{n}}$, the law of the value $X_{n}$, which lies in $\mathcal{M}_{\mathrm{fin}}$ for every $n\in\mathbb{N}$), gives the sequence of laws $(P_{X_{n}})_{n\in\mathbb{N}}$, a map $\mathbb{N}\to\mathcal{M}_{\mathrm{fin}}$ (a set, as an element of $\mathcal{M}_{\mathrm{fin}}^{\mathbb{N}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)) and so a sequence of finite measures on $(S,\mathcal{B}(S))$. We show that $\gamma$ holds if and only if

$$P_{X_{n}}\Rightarrow P_{X}.$$

Suppose $\gamma$ holds with sets $s$ and $\mu$. By $W(S,d,s,\mu)$, $s$ is a sequence of finite measures on $(S,\mathcal{B}(S))$, $\mu$ is a finite measure on it, and $s\Rightarrow\mu$. By the claim, applied to $(\Omega,\mathcal{F},P)$ and $X$, $\ell(P,X,\mu)$ gives $\mu=P_{X}$. For $n\in\mathbb{N}$, the only set $m$ with $(n,m)\in s$ is the term $s_{n}$, and the only sets $p$ and $e$ with $(n,p)\in P_{\bullet}$ and $(n,e)\in X_{\bullet}$ are $P_{n}$ and $X_{n}$; so $\ell(P_{n},X_{n},s_{n})$ holds, and by the claim $s_{n}=P_{X_{n}}$. The maps $s$ and $(P_{X_{n}})$ from $\mathbb{N}$ to $\mathcal{M}_{\mathrm{fin}}$ ($s$ maps into $\mathcal{M}_{\mathrm{fin}}$ because each $s_{n}$ is a finite measure on $(S,\mathcal{B}(S))$, by $W(S,d,s,\mu)$) thus have the same terms, so they are equal (Sequences: Enlarging the Codomain, Extensionality and the Range (ii)), and $P_{X_{n}}\Rightarrow P_{X}$. Conversely, if $P_{X_{n}}\Rightarrow P_{X}$, then $s=(P_{X_{n}})$ and $\mu=P_{X}$ satisfy $W(S,d,s,\mu)$, and by the claim $\ell(P,X,P_{X})$ and $\ell(P_{n},X_{n},P_{X_{n}})$ for every $n\in\mathbb{N}$; with the description of the sets $m$, $p$ and $e$ above, this is the bracket after $\exists s\,\exists\mu$, so $\gamma$ holds. By Convergence in Distribution of Random Elements of a Metric Space (i), $\gamma$ therefore holds if and only if $(X_{n})$ converges to $X$ in distribution. In every case $\alpha$ holds if and only if the condition of (i) holds with $S,d,(\Omega_{n}),(\mathcal{F}_{n}),(P_{n}),(X_{n}),\Omega,\mathcal{F},P,X$ the sets assigned to $x_{0},\dots,x_{9}$. So $\alpha$ is a predicative formula in $x_{0},\dots,x_{9}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing this condition.

Convergence in distribution. By Renaming and Substituting Variables in Predicative Formulas (i), with its $\varphi$ equal to $\alpha$, its $k$ equal to $10$, its $n$ equal to $q$ and $\sigma(r)=i_{r}$ for $r<10$, the formula $\alpha(x_{i_{0}},\dots,x_{i_{9}})$ is a predicative formula in $x_{0},\dots,x_{q-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{q-1}$, exactly when the condition of (i) holds for the sets assigned to $x_{i_{0}},\dots,x_{i_{9}}$. This proves (i).