Kit for def:expectation-variance

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Measurable Functions and the Lebesgue Integral: Notation, let $(\Omega,\mathcal{F})$ be a measurable space. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k,l<N$, not necessarily distinct. The parameters, each other than $x_{0},\dots,x_{N-1}$, are the set variables $\Omega$ and $\mathcal{F}$; the seventeen parameters of Kit for def:probability-space-random-variable; the parameters of Kit for def:lebesgue-integral-integrable for the measurable space $(\Omega,\mathcal{F})$; and the six parameters of Kit for def:measurable-function; the last three groups with the kinds and values given there. In the first three 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}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these parameters.

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

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

(iii) Integrable matrix-valued functions. With $P=x_{i}$, $p=x_{j}$, $q=x_{k}$ and $X=x_{l}$, the condition "$P$ is a measure on $(\Omega,\mathcal{F})$, $(\Omega,\mathcal{F},P)$ is a probability space, $p,q\in\mathbb{N}$, and $X$ lies in the set $\mathcal{L}^{1}(P;\mathbb{R}^{p\times q})$" is predicative.

(iv) The class of integrable random variables. For every measure $P$ on $(\Omega,\mathcal{F})$ such that $(\Omega,\mathcal{F},P)$ is a probability space, there is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is an integrable random variable; and $C$ is the set $\mathcal{L}^{1}(P)$.

(v) The class of integrable random vectors. For every measure $P$ on $(\Omega,\mathcal{F})$ such that $(\Omega,\mathcal{F},P)$ is a probability space and every $n\in\mathbb{N}$, there is a class $D$ such that, for every class $a$, $a\in D$ if and only if $a$ is an integrable random vector in $\mathbb{R}^{n}$; and $D$ is the set $\mathcal{L}^{1}(P;\mathbb{R}^{n})$.