Proof of Kit for def:almost-sure-convergence

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 (iii), 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_{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)).

The sequence of values at $\omega$. Let

$$\nu(\omega,u)=\Phi(u)\wedge\forall p\,\bigl(p\in\mathbb{N}\Leftrightarrow\exists t\,((p,t)\in u)\bigr)\wedge\forall p\,\forall e\,\forall t\,\bigl(((p,e)\in s\wedge(\omega,t)\in e)\Rightarrow(p,t)\in u\bigr).$$

Claim: let $(\Omega,\mathcal{F},P)$ be a probability space, $(S,d)$ a metric space, $s=(X_{n})$ a sequence of random elements of $S$ and $\omega\in\Omega$; then there is a sequence $v$ in $S$ with $v_{p}=X_{p}(\omega)$ for every $p\in\mathbb{N}$, the sequence $(X_{n}(\omega))_{n\in\mathbb{N}}$, and $v$ is the only set $u$ with $\nu(\omega,u)$. Indeed, $X_{p}(\omega)\in S$ for every $p\in\mathbb{N}$, as $X_{p}:\Omega\to S$, so Maps and Relations Given by Formulas (i), with $\mathbb{N}$, $S$ and $p\mapsto X_{p}(\omega)$ as its $a$, $b$ and $t$, gives the map $v:\mathbb{N}\to S$. The sets $p$ and $e$ with $(p,e)\in s$ are the $p\in\mathbb{N}$ with $e=X_{p}$, and then the only set $t$ with $(\omega,t)\in X_{p}$ is $X_{p}(\omega)$; so the last conjunct of $\nu(\omega,u)$ says that $(p,X_{p}(\omega))\in u$ for every $p\in\mathbb{N}$. The map $v$ satisfies $\nu(\omega,v)$: it is a function with domain $\mathbb{N}$ (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii)), and $(p,v_{p})\in v$ for $p\in\mathbb{N}$. Conversely, if $\nu(\omega,u)$ holds, then $u$ is a function with domain $\mathbb{N}$ containing $(p,X_{p}(\omega))$ for every $p\in\mathbb{N}$, so $u$ is a map $u:\mathbb{N}\to S$ with $u(p)=X_{p}(\omega)=v_{p}$ for every $p\in\mathbb{N}$, and so $u=v$, two maps on $\mathbb{N}$ with the same values being equal. This proves the claim.

The formula for almost sure convergence. Apply Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) with the set variables $S$ and $d$ as its parameters $X$ and $d$, its other parameters being those of the statement, $u$ and $z$ as its variables $s$ and $z$, and its other variables, and the auxiliary variables of $\mu$ in its formula, chosen as further set variables; let $\kappa(u,z)$ be the resulting formula. It is predicative, with free variables among $u$, $z$, $S$, $d$ and the parameters $\mathbb{N}$, $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$ and $0$. Let

$$\lambda=\exists A\,\Bigl(A\in\mathcal{F}\wedge(A,1)\in P\wedge\forall\omega\,\bigl(\omega\in A\Rightarrow\exists u\,\exists z\,(\nu(\omega,u)\wedge(\omega,z)\in X\wedge\kappa(u,z))\bigr)\Bigr)$$

and

$$\alpha(\Omega,\mathcal{F},P,S,d,s,X)=\rho(\Omega,\mathcal{F},P,S,d,X)\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 metric space, or $X$ is not a random element of $S$, then $\rho(\Omega,\mathcal{F},P,S,d,X)$ fails, and $\alpha$ fails together with the condition of (i). Let $(\Omega,\mathcal{F},P)$ be a probability space, $(S,d)$ a 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$. For a set $A$, $A\in\mathcal{F}$ says that $A$ is an event (Probability Spaces, Events and Random Elements (ii)), and then, $P$ being a map $P:\mathcal{F}\to[0,\infty]$ (Measure, Measure Space, and Probability Measure (i)) and the value of the parameter $1$ being the element $1$ of $[0,\infty]$, $(A,1)\in P$ says that $P(A)=1$. Every element $\omega$ of such an $A$ lies in $\Omega$, as $\mathcal{F}$ is a $\sigma$-algebra on $\Omega$ and so a subset of the power set of $\Omega$ (σ-Algebra and Measurable Space (i)). For such $\omega$, the only set $z$ with $(\omega,z)\in X$ is $X(\omega)\in S$, and by the claim the only set $u$ with $\nu(\omega,u)$ is the sequence $(X_{n}(\omega))$ in $S$; so the part after $\omega\in A\Rightarrow$ holds if and only if $\kappa$ holds with $u=(X_{n}(\omega))$ and $z=X(\omega)$. By Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i), applied to the metric space $(S,d)$ as the values of its parameters $X$ and $d$ (a statement holds for all values of its parameters satisfying its hypotheses, Conditions Expressed by a Predicative Formula, and Guards (i)), this is the case exactly when

$$X_{n}(\omega)\to X(\omega)\quad\text{in }(S,d),$$

as $(X_{n}(\omega))$ is a sequence in $S$ and $X(\omega)\in S$. Hence $\lambda$ holds if and only if there is an event $A$ with $P(A)=1$ such that $(X_{n}(\omega))$ converges to $X(\omega)$ in $(S,d)$ for every $\omega\in A$, that is, by Almost Sure Convergence of Random Elements of a Metric Space (i), if and only if $(X_{n})$ converges to $X$ almost surely. 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.

Almost sure convergence. 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 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}}$ almost surely. This proves (i).