Kit for def:gaussian-random-vector

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_{0},\dots,i_{8}<n$, not necessarily distinct. Let the eighteen variables of Kit for def:independence-events-rvs (its $Z$ being written $Z_{[0,\infty]}$ here) have their values there, its set variables being other than $x_{0},\dots,x_{n-1}$; let $d_{\mathbb{R}}$ and $\gamma$ be further distinct class variables with values the distance on $\mathbb{R}$ and the standard normal distribution; and let $1_{\mathbb{N}}$ be a further set variable, other than $x_{0},\dots,x_{n-1}$ and the set variables of the eighteen, with value the number one. 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 twenty-one variables as parameters.

(i) Gaussian representations. With $\Omega=x_{i_{0}}$, $\mathcal{F}=x_{i_{1}}$, $P=x_{i_{2}}$, $d=x_{i_{3}}$, $X=x_{i_{4}}$, $k=x_{i_{5}}$, $Z=x_{i_{6}}$, $m=x_{i_{7}}$ and $A=x_{i_{8}}$: the condition "$(\Omega,\mathcal{F},P)$ is a probability space, $d\in\mathbb{N}$, $X$ is a random vector in $\mathbb{R}^{d}$, and $(k,Z,m,A)$ is a Gaussian representation of $X$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Gaussian random vectors. With $\Omega=x_{i_{0}}$, $\mathcal{F}=x_{i_{1}}$, $P=x_{i_{2}}$, $d=x_{i_{3}}$ and $X=x_{i_{4}}$: the condition "$(\Omega,\mathcal{F},P)$ is a probability space, $d\in\mathbb{N}$, $X$ is a random vector in $\mathbb{R}^{d}$, and $X$ is Gaussian" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) Jointly Gaussian random variables. With $\Omega=x_{i_{0}}$, $\mathcal{F}=x_{i_{1}}$, $P=x_{i_{2}}$, $d=x_{i_{3}}$ and $X=x_{i_{4}}$: the condition "$(\Omega,\mathcal{F},P)$ is a probability space, $d\in\mathbb{N}$, $X=(X_{t})_{t\in[d]}$ is a family indexed by the segment $[d]$ in which each $X_{t}$ is a random variable, and $X_{1},\dots,X_{d}$ are jointly Gaussian" on $x_{0},\dots,x_{n-1}$ is predicative.

(iv) Gaussian random variables. With $\Omega=x_{i_{0}}$, $\mathcal{F}=x_{i_{1}}$, $P=x_{i_{2}}$ and $X=x_{i_{3}}$: the condition "$(\Omega,\mathcal{F},P)$ is a probability space, $X$ is a random variable, and $X$ is Gaussian" on $x_{0},\dots,x_{n-1}$ is predicative.