Kit for def:probability-space-random-variable

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k,l,m,p<N$, not necessarily distinct. Let $E$, $L$, $Z$, $\oplus$, $\mathbb{N}$, $R$ and $Q$ be distinct class variables with the values of the class variables $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ of Sums of Sequences in [0,∞] as Typed Terms and as a Map (i) (its $P$ being written $\oplus$ and its $N$ being written $\mathbb{N}$ here), and let $\infty$, $0$ and $1$ be distinct set variables, other than $x_{0},\dots,x_{N-1}$, whose values are the element $\infty$ of The Extended Real Line, Its Order, and [0,∞] (i) and the elements $0$ and $1$ of $[0,\infty]$ (Addition and Multiplication on [0,∞] (ii)). Let $\mathbb{R}$, $\le_{\mathbb{R}}$, $<_{\mathbb{R}}$, $+_{\mathbb{R}}$, $0_{\mathbb{R}}$, $\mathcal{B}(\mathbb{R})$ and $\mathcal{B}([0,\infty])$ be further distinct class variables with values, in this order, the set of real numbers, its order, its strict order, its addition, its zero, the Borel $\sigma$-algebra of Borel Sigma-Algebra of a Metric Space (ii) and the Borel $\sigma$-algebra of The Borel σ-Algebra of [0,∞] (ii). In the first six clauses, a condition on $x_{0},\dots,x_{N-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ as the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these seventeen variables as parameters.

(i) Probability spaces. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$ and $P=x_{k}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, and $(\Omega,\mathcal{F},P)$ is a probability space" is predicative.

(ii) Probability spaces as tuples. With $T=x_{i}$, the condition "$T$ is the tuple $\langle\Omega,\mathcal{F},P\rangle$ for some sets $\Omega$, $\mathcal{F}$ and $P$ such that $(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, and $(\Omega,\mathcal{F},P)$ is a probability space" is predicative.

(iii) Events. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$ and $A=x_{l}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, and $A$ is an event of $(\Omega,\mathcal{F},P)$" is predicative.

(iv) Random elements. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $S=x_{l}$, $d=x_{m}$ and $X=x_{p}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $d$ is a map from the Cartesian product $S\times S$ to $\mathbb{R}$, $(S,d)$ is a metric space, and $X$ is a random element of $S$" is predicative.

(v) Random variables. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$ and $X=x_{l}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, and $X$ is a random variable" is predicative.

(vi) Random vectors. With $\Omega=x_{i}$, $\mathcal{F}=x_{j}$, $P=x_{k}$, $n=x_{l}$ and $X=x_{m}$, the condition "$(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $n\in\mathbb{N}$, and $X$ is a random vector in $\mathbb{R}^{n}$" is predicative.

(vii) The class of probability spaces. There is a class $\mathcal{P}$ such that, for every class $T$, $T\in\mathcal{P}$ if and only if $T$ is the tuple $\langle\Omega,\mathcal{F},P\rangle$ for some sets $\Omega$, $\mathcal{F}$ and $P$ such that $(\Omega,\mathcal{F})$ is a measurable space, $P$ is a measure on $(\Omega,\mathcal{F})$, and $(\Omega,\mathcal{F},P)$ is a probability space.