Proof of Kit for def:probability-space-random-variable

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 sets, maps and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (i), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (v)), and so is the agreement with the current versions of the earlier versions of the definitions of $\sigma$-algebras, Borel $\sigma$-algebras and metric spaces that some cited items use (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 Metric Spaces, Convergence, Continuity and Compactness Agree (i)). The given $x_{0},\dots,x_{N-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 $N<7$; the seventeen parameters of the statement are other than these and the bound variables below, and are at their fixed values (Conditions Expressed by a Predicative Formula, and Guards (i)); $w$ and $z$ are two further distinct set variables, other than all of these. A formula taken from another item is used at the variables named, its bound variables chosen other than all of these and its parameters being the parameters of the statement with the same values; a formula with fewer parameters is one with these seventeen. Each formula below is built in $x_{0},\dots,x_{m}$ for some $m$ and then read at the positions of the clause at hand; so read, it is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the same condition at the new positions (Renaming and Substituting Variables in Predicative Formulas (i), Renaming and Substituting Variables in Predicative Formulas (ii)).

The formula for probability spaces. By Kit for def:measure-measure-space (vi), with its $n$ equal to $3$, $i=0$, $j=1$ and $k=2$, and its class variables $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$, $Q$ and set variables $\infty$, $0$, $1$ chosen to be the parameters $E$, $L$, $Z$, $\oplus$, $\mathbb{N}$, $R$, $Q$, $\infty$, $0$, $1$ of the statement, which have the values and kinds that kit prescribes, there is a predicative formula $\pi$ in $x_{0},x_{1},x_{2}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing "$(x_{0},x_{1})$ is a measurable space and $x_{2}$ is a probability measure on $(x_{0},x_{1})$". Let sets $\Omega$, $\mathcal{F}$ and $P$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $(\Omega,\mathcal{F})$ is not a measurable space, both $\pi$ and the condition of (i) with $\Omega=x_{0}$, $\mathcal{F}=x_{1}$ and $P=x_{2}$ fail. Let $(\Omega,\mathcal{F})$ be a measurable space. By Measure, Measure Space, and Probability Measure (v), $P$ is a probability measure on $(\Omega,\mathcal{F})$ if and only if $P$ is a measure on $(\Omega,\mathcal{F})$ with

$$P(\Omega)=1.$$

If $P$ is a measure on $(\Omega,\mathcal{F})$, then $\langle\Omega,\mathcal{F},P\rangle$ is a measure space (Measure, Measure Space, and Probability Measure (ii)), and by Probability Spaces, Events and Random Elements (i) it is a probability space if and only if $P(\Omega)=1$. If $P$ is not a measure on $(\Omega,\mathcal{F})$, both fail, a probability measure being a measure. Hence $\pi$ expresses the condition of (i) with $\Omega=x_{0}$, $\mathcal{F}=x_{1}$ and $P=x_{2}$; we say that $(\Omega,\mathcal{F},P)$ satisfies $\pi$.

Probability spaces. Read at the positions $i,j,k$, the formula $\pi(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (i). This proves (i).

Events. Let $\varepsilon=\pi\wedge x_{3}\in x_{1}$. It is predicative, as a conjunction of $\pi$ and an atomic formula, with free variables among $x_{0},\dots,x_{3}$ and the parameters. For sets $\Omega$, $\mathcal{F}$, $P$ and $A$ assigned to $x_{0},\dots,x_{3}$, $\varepsilon$ holds if and only if $(\Omega,\mathcal{F},P)$ satisfies $\pi$ and $A\in\mathcal{F}$, that is, by Probability Spaces, Events and Random Elements (ii), if and only if the condition of (iii) holds with $\Omega,\mathcal{F},P,A=x_{0},\dots,x_{3}$. Read at the positions $i,j,k,l$, the formula $\varepsilon(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (iii). This proves (iii).

Random variables. By Kit for def:measurable-function (ii), with its $N$ equal to $4$, $i=0$, $j=1$ and $k=3$, and its class variables $\mathbb{N}$, $R$, $\mathbb{R}$, $\mathcal{B}(\mathbb{R})$, $[0,\infty]$ and $\mathcal{B}([0,\infty])$ taken to be the parameters $\mathbb{N}$, $R$, $\mathbb{R}$, $\mathcal{B}(\mathbb{R})$, $Z$ and $\mathcal{B}([0,\infty])$ of the statement, class variables with the values that kit prescribes (our $Z$ being the set $[0,\infty]$ of The Extended Real Line, Its Order, and [0,∞] (ii), $R$ the order of The Order on Omega (i) and $\mathbb{N}$ the set of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), by Sums of Sequences in [0,∞] as Typed Terms and as a Map (i)), there is a predicative formula $\rho_{\mathbb{R}}$ in $x_{0},\dots,x_{3}$ expressing "$(x_{0},x_{1})$ is a measurable space and $x_{3}$ is a map $x_{0}\to\mathbb{R}$ that is measurable as a map into $\mathbb{R}$". Let $\upsilon=\pi\wedge\rho_{\mathbb{R}}$; it is predicative, with free variables among $x_{0},\dots,x_{3}$ and the parameters. For sets $\Omega$, $\mathcal{F}$, $P$ and $X$ assigned to $x_{0},\dots,x_{3}$, $\upsilon$ holds if and only if $(\Omega,\mathcal{F},P)$ satisfies $\pi$ and $X:\Omega\to\mathbb{R}$ is a map that is measurable as a map into $\mathbb{R}$, that is, by Probability Spaces, Events and Random Elements (iv), if and only if the condition of (v) holds with $\Omega,\mathcal{F},P,X=x_{0},\dots,x_{3}$. Read at the positions $i,j,k,l$, the formula $\upsilon(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (v). This proves (v).

Random vectors. By Kit for def:measurable-function (iii), with its $N$ equal to $5$, $i=0$, $j=1$, $k=3$ and $l=4$, and its class variables chosen as for $\rho_{\mathbb{R}}$, there is a predicative formula $\rho_{E}$ in $x_{0},\dots,x_{4}$ expressing "$(x_{0},x_{1})$ is a measurable space, $x_{3}\in\mathbb{N}$, and $x_{4}$ is a map $x_{0}\to\mathbb{R}^{x_{3}}$ that is measurable as a map into $\mathbb{R}^{x_{3}}$". Let $\nu=\pi\wedge\rho_{E}$; it is predicative, with free variables among $x_{0},\dots,x_{4}$ and the parameters. For sets $\Omega$, $\mathcal{F}$, $P$, $n$ and $X$ assigned to $x_{0},\dots,x_{4}$, $\nu$ holds if and only if $(\Omega,\mathcal{F},P)$ satisfies $\pi$, $n\in\mathbb{N}$, and $X:\Omega\to\mathbb{R}^{n}$ is a map that is measurable as a map into $\mathbb{R}^{n}$, that is, by Probability Spaces, Events and Random Elements (v), if and only if the condition of (vi) holds with $\Omega,\mathcal{F},P,n,X=x_{0},\dots,x_{4}$. Read at the positions $i,j,k,l,m$, the formula $\nu(x_{i},x_{j},x_{k},x_{l},x_{m})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (vi). This proves (vi).

The formula for the Borel $\sigma$-algebra of a metric space. By 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), with $S=x_{3}$ and $d=x_{4}$, there is a predicative formula $\mathrm{ms}(x_{3},x_{4})$ expressing "$x_{4}$ is a map from $x_{3}\times x_{3}$ to $\mathbb{R}$ and $(x_{3},x_{4})$ is a metric space", the standing hypothesis of Metric Space on the map being part of the condition as $x_{3}$ and $x_{4}$ are assigned arbitrary sets. By 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), with $B=z$, $S=x_{3}$ and $d=x_{4}$, there is a predicative formula $\mathrm{bo}(z,x_{3},x_{4})$ expressing "$(x_{3},x_{4})$ is a metric space and $z\in\mathcal{B}(x_{3},x_{4})$", with the Borel $\sigma$-algebra $\mathcal{B}(x_{3},x_{4})$. The parameters of these formulas have the values of the parameters $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$, $0_{\mathbb{R}}$ and $\mathbb{N}$ of the statement, and are taken to be these. Let

$$\beta=\mathrm{ms}(x_{3},x_{4})\wedge\forall z\,\bigl(z\in x_{6}\Leftrightarrow\mathrm{bo}(z,x_{3},x_{4})\bigr).$$

As $\mathrm{ms}$ and $\mathrm{bo}$ are predicative and the added quantifier $\forall z$ is over a set variable, $\beta$ is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), with free variables among $x_{3}$, $x_{4}$, $x_{6}$ and the parameters. Let sets $S$, $d$ and $\mathcal{G}$ be assigned to $x_{3}$, $x_{4}$ and $x_{6}$; here and in the next paragraph, "$(S,d)$ is a metric space" includes that $d:S\times S\to\mathbb{R}$ is a map. If $(S,d)$ is not a metric space, $\beta$ fails. If it is one, $\mathcal{B}(S,d)$ is the $\sigma$-algebra on $S$ generated by the set $\mathcal{T}_{d}$ of open subsets of $S$ (Borel Sigma-Algebra of a Metric Space (i)), so it is a $\sigma$-algebra on $S$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (iii), hence a set, and $(S,\mathcal{B}(S,d))$ is a measurable space (σ-Algebra and Measurable Space (i), σ-Algebra and Measurable Space (ii)). The second conjunct of $\beta$ then says that every set $z$ satisfies $z\in\mathcal{G}\Leftrightarrow z\in\mathcal{B}(S,d)$, which holds exactly when $\mathcal{G}=\mathcal{B}(S,d)$. So $\beta$ holds if and only if $(S,d)$ is a metric space and

$$\mathcal{G}=\mathcal{B}(S,d).$$

Random elements. By Kit for def:measurable-function (i), with its $N$ equal to $7$, its indices $i,j,k,l,m$ equal to $0,1,3,6,5$, and its class variables chosen as for $\rho_{\mathbb{R}}$, there is a predicative formula $\varphi$ in $x_{0},\dots,x_{6}$ expressing "$(x_{0},x_{1})$ and $(x_{3},x_{6})$ are measurable spaces and $x_{5}$ is a map $x_{0}\to x_{3}$ that is $x_{1}/x_{6}$-measurable". Let

$$\rho=\pi\wedge\exists x_{6}\,\bigl(\beta\wedge\varphi\bigr).$$

It is predicative, with free variables among $x_{0},\dots,x_{5}$ and the parameters. Let sets $\Omega$, $\mathcal{F}$, $P$, $S$, $d$ and $X$ be assigned to $x_{0},\dots,x_{5}$. If $(S,d)$ is not a metric space, then $\beta$ fails for every set assigned to $x_{6}$, so $\rho$ fails, and so does the condition of (iv). Let $(S,d)$ be a metric space. Then the only set $\mathcal{G}$ that satisfies $\beta$ when assigned to $x_{6}$ is $\mathcal{B}(S,d)$, a set with $(S,\mathcal{B}(S,d))$ a measurable space, as shown above. So $\rho$ holds if and only if $(\Omega,\mathcal{F},P)$ satisfies $\pi$ and $X:\Omega\to S$ is a map that is $\mathcal{F}/\mathcal{B}(S,d)$-measurable (the measurability of $(\Omega,\mathcal{F})$ being part of $\pi$), that is, by Probability Spaces, Events and Random Elements (iii), if and only if $(\Omega,\mathcal{F},P)$ satisfies $\pi$ and $X$ is a random element of $S$. Hence $\rho$ expresses the condition of (iv) with $\Omega,\mathcal{F},P,S,d,X=x_{0},\dots,x_{5}$. Read at the positions $i,j,k,l,m,p$, the formula $\rho(x_{i},x_{j},x_{k},x_{l},x_{m},x_{p})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (iv). This proves (iv).

Probability spaces as tuples. Read at the positions $1,2,3$, the formula $\pi(x_{1},x_{2},x_{3})$ is a predicative formula in $x_{0},\dots,x_{3}$ that holds exactly when $(x_{1},x_{2},x_{3})$ satisfies $\pi$. Let

$$\theta=\exists x_{1}\,\exists x_{2}\,\exists x_{3}\,\exists w\,\bigl(w=(x_{1},x_{2})\wedge x_{0}=(w,x_{3})\wedge\pi(x_{1},x_{2},x_{3})\bigr).$$

The formulas $w=(x_{1},x_{2})$ and $x_{0}=(w,x_{3})$ are predicative and, for sets assigned, say that $w$ is the ordered pair of $x_{1}$ and $x_{2}$ and $x_{0}$ that of $w$ and $x_{3}$, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii). So $\theta$ is predicative, its quantifiers being over set variables, with free variables among $x_{0}$ and the parameters. By The Ordered Pair of Two Sets and Nested Tuples (ii), $((\Omega,\mathcal{F}),P)$ is the tuple $\langle\Omega,\mathcal{F},P\rangle$. For a set $T$ assigned to $x_{0}$, $\theta$ therefore holds if and only if $T=\langle\Omega,\mathcal{F},P\rangle$ for some sets $\Omega$, $\mathcal{F}$ and $P$ such that $(\Omega,\mathcal{F},P)$ satisfies $\pi$. This is the condition of (ii), since $\Omega$, $\mathcal{F}$ and $P$ range over sets there as here. Read at the position $i$, the formula $\theta(x_{i})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (ii). This proves (ii).

The class of probability spaces. By The Class Comprehension Theorem for Predicative Formulas (i), applied to $\theta$ with the single set variable $x_{0}$ and the parameters of the statement, there is a class $\mathcal{P}$ such that $T\in\mathcal{P}$ if and only if $T=\langle\Omega,\mathcal{F},P\rangle$ for a probability space $(\Omega,\mathcal{F},P)$ as in (vii), for every set $T$ and so for every class $T$ (the tuple $\langle x_{0}\rangle$ being $x_{0}$, elements of classes being sets, and a tuple of sets being a set, The Ordered Pair of Two Sets and Nested Tuples (ii)). This proves (vii).