Proof of Kit for def:convergence-modes

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. 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 versions of definitions read by published results cited below with their current versions (The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (i), The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (ii), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (ii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (ii), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (iii), The Earlier and the New Versions of the Definitions of Probability Spaces, Laws, Expectation, Independence and Modes of Convergence 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_{6}$ are distinct also when $q<7$; the letters $\Omega$, $\mathcal{F}$, $P$, $S$, $d$, $s$ and $X$ denote $x_{0},\dots,x_{6}$, every other letter used below as a variable denotes a further set variable, distinct letters denoting distinct variables, none of them a parameter, and bound variables of formulas taken from other results are renamed where necessary so that none is captured. The value of the parameter $\mathbb{N}$ is the set of natural numbers (Sums of Sequences in [0,∞] as Typed Terms and as a Map (i)), from which sequences are maps (Sequences (i)).

Random elements and sequences of random elements. By Kit for def:probability-space-random-variable (iv), with its $N$ equal to $6$ and its indices $i,j,k,l,m,p$ equal to $0,\dots,5$, and by renaming, there is a predicative formula $\rho(\Omega,\mathcal{F},P,S,d,e)$ that holds if and only if $(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on it, $(\Omega,\mathcal{F},P)$ is a probability space, $d$ is a map $S\times S\to\mathbb{R}$, $(S,d)$ is a metric space and $e$ is a random element of $S$. The first two parts are the standing hypotheses of Probability Spaces, Events and Random Elements (i) and the fourth is that of Metric Space (vi); so $\rho(\Omega,\mathcal{F},P,S,d,e)$ holds if and only if $(\Omega,\mathcal{F},P)$ is a probability space, $(S,d)$ is a metric space and $e$ is a random element of $S$, that is, $e\in M$ for the set $M=\mathrm{Meas}(\Omega,\mathcal{F};S,\mathcal{B}(S))$ (Probability Spaces, Events and Random Elements (iii)). 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

$$\eta(s)=\Phi(s)\wedge\forall p\,\bigl(p\in\mathbb{N}\Leftrightarrow\exists e\,((p,e)\in s)\bigr)\wedge\forall p\,\forall e\,\bigl((p,e)\in s\Rightarrow\rho(\Omega,\mathcal{F},P,S,d,e)\bigr).$$

When $(\Omega,\mathcal{F},P)$ is a probability space and $(S,d)$ a metric space, $\eta(s)$ holds exactly when $s$ is a function with domain $\mathbb{N}$ and values in $M$, that is, a map $s:\mathbb{N}\to M$, a sequence of random elements of $S$ (Sequences (i)).

Separable metric spaces. By Kit for def:separable-metric (i), with its $n$ equal to $7$ and its $i$, $j$ equal to $3$, $4$, there is a predicative formula $\chi(S,d)$ in $x_{0},\dots,x_{6}$ that holds if and only if $d$ is a map $S\times S\to\mathbb{R}$, $(S,d)$ is a metric space and $(S,d)$ is separable. As the first part is the standing hypothesis of Metric Space (vi), $\chi(S,d)$ holds if and only if $(S,d)$ is a separable metric space.

The events $\{d(X_{n},X)>\varepsilon\}$ and their probabilities. Let

$$\Lambda(e,\varepsilon,t)=\exists w\,\Bigl(\forall\omega\,\bigl(\omega\in w\Leftrightarrow(\omega\in\Omega\wedge\exists a\,\exists c\,\exists r\,((\omega,a)\in e\wedge(\omega,c)\in X\wedge((a,c),r)\in d\wedge(\varepsilon,r)\in{<_{\mathbb{R}}}))\bigr)\wedge(w,t)\in P\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), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv)). *Claim: let $(\Omega,\mathcal{F},P)$ be a probability space, $(S,d)$ a separable metric space, $e$ and $X$ random elements of $S$, and $\varepsilon$ a real number with $\varepsilon>0$; then the set

$$G=\{d(e,X)>\varepsilon\}=\{\omega\in\Omega:\ d(e(\omega),X(\omega))>\varepsilon\}$$

of Probability Spaces: Notation (iii) is an event, its probability $P(G)$ is a real number, and for every set $t$, $\Lambda(e,\varepsilon,t)$ holds if and only if $t=P(G)$.* Indeed, the map $d(e,X):\Omega\to\mathbb{R}$, $\omega\mapsto d(e(\omega),X(\omega))$, of Probability Spaces: Notation (iv) is a random variable by The Distance of Two Random Elements of a Separable Metric Space Is a Random Variable (i), that is, an $\mathcal{F}/\mathcal{B}(\mathbb{R})$-measurable map (Probability Spaces, Events and Random Elements (iv), Measurable Map, and the Set of Measurable Maps (iii)). The ray $(\varepsilon,\infty)=\{x\in\mathbb{R}:\varepsilon<x\}$ of Intervals of the Real Line (iii) belongs to $\mathcal{B}(\mathbb{R})$ by Intervals Are Borel, and Rays, Half-Open Intervals and Rational Intervals Generate the Borel Sigma-Algebra of the Real Line (ii), and its preimage under $d(e,X)$ is $G$; so $G\in\mathcal{F}$ by Measurable Map, and the Set of Measurable Maps (i), that is, $G$ is an event (Probability Spaces, Events and Random Elements (ii)), and in particular a set. As $P$ is a map $P:\mathcal{F}\to[0,\infty]$ (Measure, Measure Space, and Probability Measure (i)), $P(G)\in[0,\infty]$, and as $G\subseteq\Omega$ and $\Omega\in\mathcal{F}$ (σ-Algebra and Measurable Space (i)), Basic Properties of a Measure (iii), applied to the measure space $(\Omega,\mathcal{F},P)$, gives

$$P(G)\le P(\Omega)=1<\infty,$$

where $P(\Omega)=1$ by Probability Spaces, Events and Random Elements (i), and $1<\infty$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii), since $1$ is real; so $P(G)$ is a real number by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii). Now let $\omega$ be a set. If $\omega\in\Omega$, the only sets $a$ and $c$ with $(\omega,a)\in e$ and $(\omega,c)\in X$ are $e(\omega),X(\omega)\in S$; as $d$ is a map $S\times S\to\mathbb{R}$, the only set $r$ with $((e(\omega),X(\omega)),r)\in d$ is $d(e(\omega),X(\omega))$; and $(\varepsilon,r)\in{<_{\mathbb{R}}}$ then says that $\varepsilon<d(e(\omega),X(\omega))$. So the right-hand side of the equivalence holds if and only if $\omega\in G$. Elements of classes being sets, by the axiom of extensionality a set $w$ satisfies the first conjunct inside $\exists w$ if and only if $w=G$; and as $G\in\mathcal{F}$, $(G,t)\in P$ holds if and only if $t=P(G)$. This proves the claim.

The formula for convergence in probability. Apply Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) to the metric space $(\mathbb{R},d_{\mathbb{R}})$ of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv), its parameters being those of the statement, with $u$ as its variable $s$, and put the parameter $0$ for its variable $z$ (Renaming and Substituting Variables in Predicative Formulas (iii)); let $\kappa(u)$ be the resulting formula. It is predicative, and by Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (iv) it holds if and only if $u$ is a sequence in $\mathbb{R}$ that converges to $0$. Let

$$\lambda=\forall\varepsilon\,\Bigl(\bigl(\varepsilon\in\mathbb{R}\wedge(0,\varepsilon)\in{<_{\mathbb{R}}}\bigr)\Rightarrow\exists u\,\bigl(\kappa(u)\wedge\forall m\,\forall e\,\forall t\,(((m,e)\in s\wedge(m,t)\in u)\Rightarrow\Lambda(e,\varepsilon,t))\bigr)\Bigr)$$

and

$$\alpha(\Omega,\mathcal{F},P,S,d,s,X)=\rho(\Omega,\mathcal{F},P,S,d,X)\wedge\chi(S,d)\wedge\eta(s)\wedge\lambda.$$

It is predicative, with free variables among $x_{0},\dots,x_{6}$ and the parameters. Let sets $\Omega$, $\mathcal{F}$, $P$, $S$, $d$, $s$ and $X$ be assigned to $x_{0},\dots,x_{6}$. If $(\Omega,\mathcal{F},P)$ is not a probability space, or $(S,d)$ is not a separable metric space, or $X$ is not a random element of $S$, then $\rho(\Omega,\mathcal{F},P,S,d,X)$ or $\chi(S,d)$ fails, and $\alpha$ fails together with the condition of (i). Let $(\Omega,\mathcal{F},P)$ be a probability space, $(S,d)$ a separable metric space and $X$ a random element of $S$. If $s$ is not a sequence of random elements of $S$, then $\eta(s)$ fails, and again both $\alpha$ and the condition fail. Let now $s=(X_{n})$ be a sequence of random elements of $S$. The sets $\varepsilon$ satisfying the antecedent in $\lambda$ are the real numbers $\varepsilon>0$; let $\varepsilon$ be one. For a set $u$, $\kappa(u)$ says that $u$ is a sequence in $\mathbb{R}$ converging to $0$, and then, for $m\in\mathbb{N}$, the only set $t$ with $(m,t)\in u$ is $u_{m}$; the sets $m$ and $e$ with $(m,e)\in s$ are the $m\in\mathbb{N}$ with $e=X_{m}$. So by the claim, with $X_{m}$ as its $e$, the part after $\exists u$ says that $u$ is a sequence in $\mathbb{R}$ converging to $0$ with

$$u_{m}=P\bigl(d(X_{m},X)>\varepsilon\bigr)\qquad(m\in\mathbb{N}).$$

As each $P(d(X_{m},X)>\varepsilon)$ is a real number by the claim, Maps and Relations Given by Formulas (i), with $\mathbb{N}$, $\mathbb{R}$ and $m\mapsto P(d(X_{m},X)>\varepsilon)$ as its $a$, $b$ and $t$, gives such a sequence, the sequence $(P(d(X_{n},X)>\varepsilon))_{n\in\mathbb{N}}$, and by Sequences: Enlarging the Codomain, Extensionality and the Range (ii) it is the only one. So the part after $\Rightarrow$ in $\lambda$ holds if and only if

$$P\bigl(d(X_{n},X)>\varepsilon\bigr)\to0\qquad(n\to\infty),$$

convergence of real numbers as in Convergent Sequences of Real Numbers (i). Hence $\lambda$ holds if and only if this holds for every real $\varepsilon>0$, that is, by Convergence in Probability (i), if and only if $(X_{n})$ converges to $X$ in probability. In every case $\alpha$ holds if and only if the condition of (i) holds with $\Omega,\mathcal{F},P,S,d,(X_{n}),X$ the sets assigned to $x_{0},\dots,x_{6}$. So $\alpha$ is a predicative formula in $x_{0},\dots,x_{6}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing this condition.

Convergence in probability. By Renaming and Substituting Variables in Predicative Formulas (i), with its $\varphi$ equal to $\alpha$, its $k$ equal to $7$, its $n$ equal to $q$ and $\sigma(m)=i_{m}$ for $m<7$, the formula $\alpha(x_{i_{0}},\dots,x_{i_{6}})$ 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 $(x_{i_{0}},x_{i_{1}},x_{i_{2}})$ is a probability space, $(x_{i_{3}},x_{i_{4}})$ is a separable metric space, $x_{i_{5}}$ is a sequence of random elements of $x_{i_{3}}$, $x_{i_{6}}$ is a random element of $x_{i_{3}}$ and $x_{i_{5}}$ converges to $x_{i_{6}}$ in probability. This proves (i).