Proof of Kit for def:gaussian-random-vector

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 (including maps given by functional predicative relations), natural numbers and predicative formulas (including renaming and substitution of variables) are used without comment, values of maps being read off pairs (for a map $F$ and an element $a$ of its domain, $F(a)$ is the only set $b$ with $(a,b)\in F$) (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iv), 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 natural numbers, probability spaces, random variables, random vectors, laws, independence, metric spaces, $\sigma$-algebras, Borel $\sigma$-algebras, measures, Euclidean space, real matrices and finite sums that some cited items use (The Earlier and the New Versions of the Definitions of the Natural Numbers, the Complex Numbers, the Conjugate and the Modulus Agree, and the Two Versions of Real Correspond (i), The Earlier and the New Versions of the Definitions of Probability Spaces, Laws, Expectation, Independence and Modes of Convergence Agree (i), The Earlier and the New Versions of the Definitions of Probability Spaces, Laws, Expectation, Independence and Modes of Convergence Agree (ii), The Earlier and the New Versions of the Definitions of Probability Spaces, Laws, Expectation, Independence and Modes of Convergence Agree (iv), 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 σ-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 σ-Algebras, Measures, Measurable Functions and Integrals Agree (iii), The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i), The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (ii), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (vi)). Formulas are first written in distinct set variables $x_{0},x_{1},\dots$ extending the given ones: $\Omega$, $\mathcal{F}$, $P$, $d$, $X$, $k$, $Z$, $m$ and $A$ denote $x_{0},\dots,x_{8}$, every other letter used as a set variable denotes one of $x_{9},x_{10},\dots$, distinct letters denoting distinct variables, the variables beyond $x_{n-1}$ being chosen other than the parameters, and bound variables of formulas taken from other items are renamed so that none is captured; the last paragraph moves the formulas to the positions $i_{0},\dots,i_{8}$. The parameters are the twenty-one of the statement, the class variable $Z$ of Kit for def:independence-events-rvs (ii), with value $[0,\infty]$, being written $Z_{[0,\infty]}$ as in the statement. Seventeen of the eighteen parameters of that kit are those of Kit for def:probability-space-random-variable (vi) with the same values, and the eighteenth is $\cdot_{\mathbb{R}}$; among the eighteen are the class variables $\mathbb{N}$, $R$, $Q$, $\mathbb{R}$, $+_{\mathbb{R}}$ and $\cdot_{\mathbb{R}}$, for the set of natural numbers, which is the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), the order and the addition of $\mathbb{N}_{0}$, the set of real numbers and its addition and multiplication, and the set variable $0$, for the element $0$ of $[0,\infty]$.

Formulas from the kits. By Kit for def:probability-space-random-variable (i), Kit for def:probability-space-random-variable (v) and Kit for def:probability-space-random-variable (vi), each applied with its $N$ equal to the number of its displayed letters and its indices $0,1,\dots$, and renaming, there are predicative formulas $\Pi(o,f,p)$, $\rho(o,f,p,y)$ and $V(o,f,p,r,x)$, with parameters among the seventeen, such that for sets $o,f,p,y,r,x$: $\Pi(o,f,p)$ holds if and only if $(o,f,p)$ is a probability space; $\rho(o,f,p,y)$ if and only if moreover $y$ is a random variable on it; and $V(o,f,p,r,x)$ if and only if $(o,f,p)$ is a probability space, $r\in\mathbb{N}$ and $x$ is a random vector in $\mathbb{R}^{r}$ on it. (The kits' further conjuncts, that $(o,f)$ is a measurable space and $p$ a measure on it, follow from $(o,f,p)$ being a probability space, by Probability Spaces, Events and Random Elements (i) and Measure, Measure Space, and Probability Measure (ii).) By Kit for def:independence-events-rvs (ii), applied in the same way, there is a predicative formula $I(o,f,p,j,s,e,y)$, with parameters among the eighteen, that holds if and only if $(o,f,p)$ is a probability space, $s$, $e$ and $y$ are families indexed by $j$, for every $t\in j$ the value $e_{t}$ is a map $e_{t}:s_{t}\times s_{t}\to\mathbb{R}$, $(s_{t},e_{t})$ is a metric space and $y_{t}$ is a random element of $s_{t}$, and $(y_{t})_{t\in j}$ is independent.

Notation for formulas. $\Phi(F)$ and $\mu(F,a,b)$, saying that $F$ is a function and a map $F:a\to b$, are the formulas 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 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 $\Phi_{j}(F)$ is $\Phi(F)\wedge\forall t\,(t\in j\Leftrightarrow\exists a\,((t,a)\in F))$, saying that $F$ is a function with domain $j$, that is, a family indexed by $j$. $c=[q]$ denotes the predicative formula $\mathrm{seg}(c,q)$ of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), its class variables $Y$ and $R$ being taken as $\mathbb{N}$ and $R$, which for $q\in\mathbb{N}_{0}$ holds if and only if $c=[q]$; $u\in[q]$, "$u:[q]\to\mathbb{R}$" and "$M\in\mathbb{R}^{q\times r}$" abbreviate $\exists c\,(c=[q]\wedge u\in c)$, $\exists c\,(c=[q]\wedge\mu(u,c,\mathbb{R}))$ and the formula saying that $M$ is a map into $\mathbb{R}$ from the set of the pairs $(i,j)$ with $i\in[q]$ and $j\in[r]$; for $q,r\in\mathbb{N}$ the last two say $u\in\mathbb{R}^{q}$ and that $M$ is a real $q\times r$ matrix (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii), Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i)). $\Sigma(s,q,u)$ is the predicative formula $q\in\mathbb{N}\wedge u:[q]\to\mathbb{R}\wedge\mathrm{it}(s,q,u)$, where $\mathrm{it}$ is the formula of Iterated Operations Are Given by a Predicative Formula (i) with its class variables $X$, $F$, $Y$, $R$ and $P$ taken as $\mathbb{R}$, $+_{\mathbb{R}}$, $\mathbb{N}$, $R$ and $Q$; so $\Sigma(s,q,u)$ holds if and only if $q\in\mathbb{N}$, $u:[q]\to\mathbb{R}$ and $s=\sum_{l=1}^{q}u_{l}$, the finite sum being the iterated operation of $+_{\mathbb{R}}$. The parameters of $\mathrm{seg}$ and $\Sigma$ are among those named above, hence among the parameters of the statement. All formulas displayed below are predicative (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), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv)), every quantifier added being over a set variable.

Standard normal random variables. Let

$$\nu(p,y)=\forall B\,\forall v\,\Bigl((B,v)\in\gamma\Rightarrow\exists w\,\bigl(\forall u\,(u\in w\Leftrightarrow\exists q\,(q\in B\wedge(u,q)\in y))\wedge(w,v)\in p\bigr)\Bigr).$$

Claim 1: for a probability space $(o,f,p)$ and a random variable $y$ on it, $\nu(p,y)$ holds if and only if $y$ is standard normal. The measure $\gamma$ on $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ (Standard Normal Distribution (ii)) is a map $\gamma:\mathcal{B}(\mathbb{R})\to[0,\infty]$ (Measure, Measure Space, and Probability Measure (i)). Let $B\in\mathcal{B}(\mathbb{R})$. As $\mathcal{B}(\mathbb{R})$ is the Borel $\sigma$-algebra of $(\mathbb{R},d_{\mathbb{R}})$ (Borel Sigma-Algebra of a Metric Space (ii)), $y$ is a random element of $\mathbb{R}$ (Probability Spaces, Events and Random Elements (iv)), so $y^{-1}(B)\in f$ (Probability Spaces, Events and Random Elements (iii), Measurable Map, and the Set of Measurable Maps (i)). For a set $u$, $\exists q\,(q\in B\wedge(u,q)\in y)$ holds if and only if $u\in o$ and $y(u)\in B$, that is, $u\in y^{-1}(B)$; so by the axiom of extensionality the only set $w$ satisfying the first conjunct after $\exists w$ is $y^{-1}(B)$. Hence, $\gamma$ and $p:f\to[0,\infty]$ being maps, $\nu(p,y)$ holds if and only if

$$\gamma(B)=p\bigl(y^{-1}(B)\bigr)=p_{y}(B)\qquad(B\in\mathcal{B}(\mathbb{R})),$$

the second equality being The Law of a Random Element (i). As $\gamma$ and the law $p_{y}$, a probability measure on $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ by the same definition, are maps $\mathcal{B}(\mathbb{R})\to[0,\infty]$, this holds if and only if $p_{y}=\gamma$, that is, if and only if $y$ is standard normal (Standard Normal Distribution (iii)).

Standard normal vectors. Let $\sigma(o,f,p,r,z)$ be the formula $V(o,f,p,r,z)\wedge\beta$, where

$$\begin{aligned} \beta={}&\exists j\,\exists s\,\exists e\,\exists y\,\Bigl(j=[r]\wedge\Phi_{j}(s)\wedge\Phi_{j}(e)\wedge\Phi_{j}(y)\wedge I(o,f,p,j,s,e,y)\\ &\quad\wedge\forall t\,\forall a\,\forall b\,\forall c\,\bigl((t\in j\wedge(t,a)\in s\wedge(t,b)\in e\wedge(t,c)\in y)\Rightarrow(a=\mathbb{R}\wedge b=d_{\mathbb{R}}\wedge\rho(o,f,p,c)\wedge\nu(p,c)\wedge\kappa(t,c))\bigr)\Bigr),\\ \kappa(t,c)={}&\forall\omega\,\forall h\,\forall g\,\bigl(((\omega,h)\in z\wedge(t,g)\in h)\Rightarrow(\omega,g)\in c\bigr). \end{aligned}$$

Claim 2: for a probability space $(o,f,p)$, $r\in\mathbb{N}$ and a random vector $z$ in $\mathbb{R}^{r}$ on it, $\beta$ holds if and only if $z$ is a standard normal vector. For $t\in[r]$ let $z_{t}:o\to\mathbb{R}$, $\omega\mapsto z(\omega)_{t}$, be the $t$-th coordinate of $z$, a random variable by Random Vectors: Coordinates, Functions, Pairs and Almost-Sure Equality (i). For $t\in[r]$ and a map $c:o\to\mathbb{R}$, $\kappa(t,c)$ holds if and only if $c(\omega)=z(\omega)_{t}$ for every $\omega\in o$, that is, if and only if $c=z_{t}$.

Suppose $\beta$ holds with sets $j,s,e,y$. Then $j=[r]$, and $s$, $e$ and $y$ are families indexed by $[r]$; let $t\in[r]$. Then $s_{t}=\mathbb{R}$ and $e_{t}=d_{\mathbb{R}}$; $y_{t}$ is a random variable, in particular a map $y_{t}:o\to\mathbb{R}$, so $y_{t}=z_{t}$; and $z_{t}$ is standard normal, by Claim 1. By $I(o,f,p,j,s,e,y)$, the family $(z_{t})_{t\in[r]}$ of the coordinates of $z$ is independent as a family of random elements of $(\mathbb{R},d_{\mathbb{R}})$ (Independence of Events and of Random Elements (ii)). So $z$ is a standard normal vector (Standard Normal Vectors and the Standard Normal Distribution on ℝᵏ (iii)).

Conversely, let $z$ be a standard normal vector. Let $j=[r]$, let $s$ and $e$ be the constant maps on $[r]$ with values the sets $\mathbb{R}$ and $d_{\mathbb{R}}$, and let $y$ be the map $t\mapsto z_{t}$ on $[r]$, into the power set of $o\times\mathbb{R}$, given by the predicative relation $\mu(c,o,\mathbb{R})\wedge\kappa(t,c)$, which for $t\in[r]$ holds for $c=z_{t}$ only. These are families indexed by $[r]$. For $t\in[r]$, $d_{\mathbb{R}}$ is a metric on $\mathbb{R}$ (The Absolute Value Metric on the Real Numbers (i)), so it is a map $d_{\mathbb{R}}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ and $(\mathbb{R},d_{\mathbb{R}})$ is a metric space (Metric Space (vi)); $z_{t}$ is a random variable, hence a random element of $\mathbb{R}$, and standard normal, so $\rho(o,f,p,z_{t})$, $\nu(p,z_{t})$ (Claim 1) and $\kappa(t,z_{t})$ hold; and the coordinates being independent, $I(o,f,p,j,s,e,y)$ holds. So $\beta$ holds. This proves Claim 2; hence $\sigma(o,f,p,r,z)$ holds if and only if $(o,f,p)$ is a probability space, $r\in\mathbb{N}$, and $z$ is a standard normal vector in $\mathbb{R}^{r}$ on it.

The affine identity. Let

$$\begin{aligned} \alpha(x,z)={}&\forall i\,\forall a\,\forall c\,\Bigl((i\in[d]\wedge(i,a)\in x\wedge(i,c)\in m)\Rightarrow\exists u\,\exists s\,\bigl(u:[k]\to\mathbb{R}\\ &\quad\wedge\forall j\,\forall g\,\forall h\,((j\in[k]\wedge((i,j),g)\in A\wedge(j,h)\in z)\Rightarrow\exists l\,(((g,h),l)\in\cdot_{\mathbb{R}}\wedge(j,l)\in u))\\ &\quad\wedge\Sigma(s,k,u)\wedge((c,s),a)\in+_{\mathbb{R}}\bigr)\Bigr). \end{aligned}$$

Claim 3: let $d,k\in\mathbb{N}$, $m\in\mathbb{R}^{d}$, $A\in\mathbb{R}^{d\times k}$, $x\in\mathbb{R}^{d}$ and $z\in\mathbb{R}^{k}$. Then $\alpha(x,z)$ holds if and only if $x=m+Az$. Let $i\in[d]$, so that $a=x_{i}$ and $c=m_{i}$. The second conjunct after $\exists u\,\exists s$ says that $u(j)=A_{ij}z_{j}$ for every $j\in[k]$; the map $u^{(i)}:[k]\to\mathbb{R}$, $j\mapsto A_{ij}z_{j}$, exists, and it is the only map $[k]\to\mathbb{R}$ satisfying this conjunct. The only $s$ with $\Sigma(s,k,u^{(i)})$ is

$$\sum_{j=1}^{k}A_{ij}z_{j}=(Az)_{i}$$

(Matrix-Vector Product (i)), and the last conjunct then says $x_{i}=m_{i}+(Az)_{i}=(m+Az)_{i}$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iv)). So $\alpha(x,z)$ holds if and only if $x_{i}=(m+Az)_{i}$ for every $i\in[d]$, that is (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii)), if and only if $x=m+Az$.

Almost-sure equalities. Let

$$\begin{aligned} \varepsilon_{0}(w)={}&\exists B\,\bigl(B\in\mathcal{F}\wedge(B,0)\in P\wedge\forall\omega\,\forall x\,((\omega\in\Omega\wedge(\omega,x)\in X\wedge\neg\,x=w)\Rightarrow\omega\in B)\bigr),\\ \varepsilon={}&\exists B\,\bigl(B\in\mathcal{F}\wedge(B,0)\in P\wedge\forall\omega\,\forall x\,\forall z\,((\omega\in\Omega\wedge(\omega,x)\in X\wedge(\omega,z)\in Z\wedge\neg\,\alpha(x,z))\Rightarrow\omega\in B)\bigr). \end{aligned}$$

Claim 4: let $(\Omega,\mathcal{F},P)$ be a probability space, $d\in\mathbb{N}$ and $X$ a random vector in $\mathbb{R}^{d}$ on it. For $w\in\mathbb{R}^{d}$, $\varepsilon_{0}(w)$ holds if and only if $X=w$ almost surely. If moreover $k\in\mathbb{N}$, $Z$ is a random vector in $\mathbb{R}^{k}$, $m\in\mathbb{R}^{d}$ and $A\in\mathbb{R}^{d\times k}$, then $\varepsilon$ holds if and only if $X=m+AZ$ almost surely. For $\omega\in\Omega$, $X(\omega)\in\mathbb{R}^{d}$ and $Z(\omega)\in\mathbb{R}^{k}$, and by Claim 3, $\alpha(X(\omega),Z(\omega))$ holds if and only if $X(\omega)=m+AZ(\omega)$, the value at $\omega$ of the function $m+AZ$ (Probability Spaces: Notation (iv)). Let $N_{\neq}$ be the class of the $\omega\in\Omega$ with $X(\omega)\neq(m+AZ)(\omega)$. Then $\varepsilon$ holds if and only if there is $B\in\mathcal{F}$ with $P(B)=0$ and $N_{\neq}\subseteq B$, that is, if and only if $N_{\neq}$ is $P$-null (Null Set of a Measure (i)), which means that $X=m+AZ$ holds $P$-almost everywhere (A Property Holding Almost Everywhere (i)), that is, almost surely. The same argument, with the constant function $w$ in place of $m+AZ$ and without $Z$, gives the assertion on $\varepsilon_{0}(w)$.

Gaussian representations. Let

$$\Xi=V(\Omega,\mathcal{F},P,d,X)\wedge\sigma(\Omega,\mathcal{F},P,k,Z)\wedge m:[d]\to\mathbb{R}\wedge A\in\mathbb{R}^{d\times k}\wedge\varepsilon,$$

a predicative formula whose free variables are among $x_{0},\dots,x_{8}$ and the parameters. Let sets be assigned to $x_{0},\dots,x_{8}$. If $V(\Omega,\mathcal{F},P,d,X)$ fails, then $\Xi$ fails together with the condition of (i). Let it hold. By Claim 2, $\sigma(\Omega,\mathcal{F},P,k,Z)$ holds if and only if $k\in\mathbb{N}$ and $Z$ is a standard normal vector in $\mathbb{R}^{k}$ (a random vector, by Standard Normal Vectors and the Standard Normal Distribution on ℝᵏ (iii)); the next two conjuncts say $m\in\mathbb{R}^{d}$ and $A\in\mathbb{R}^{d\times k}$; and when all these hold, $\varepsilon$ holds if and only if $X=m+AZ$ almost surely, by Claim 4. So $\Xi$ holds if and only if $k$, $Z$, $m$ and $A$ are as in the second case of Gaussian Random Vectors and Jointly Gaussian Random Variables (i), that is, if and only if $(k,Z,m,A)$ is a Gaussian representation of $X$ (Gaussian Random Vectors and Jointly Gaussian Random Variables (ii)). So $\Xi$ expresses the condition of (i) with $\Omega,\dots,A$ at $x_{0},\dots,x_{8}$.

Gaussian random vectors. Let

$$G(\Omega,\mathcal{F},P,d,X)=V(\Omega,\mathcal{F},P,d,X)\wedge\Bigl(\exists w\,\bigl(w:[d]\to\mathbb{R}\wedge\varepsilon_{0}(w)\bigr)\vee\exists k\,\exists Z\,\exists m\,\exists A\,\Xi\Bigr),$$

whose free variables are among $x_{0},\dots,x_{4}$ and the parameters. When $V(\Omega,\mathcal{F},P,d,X)$ holds, the first disjunct holds, by Claim 4, if and only if $X=w$ almost surely for some $w\in\mathbb{R}^{d}$, and the second, by the previous paragraph, if and only if $X$ has a Gaussian representation. By Gaussian Random Vectors and Jointly Gaussian Random Variables (i), $G$ therefore expresses the condition of (ii) with $\Omega,\mathcal{F},P,d,X$ at $x_{0},\dots,x_{4}$.

Jointly Gaussian random variables. Let $J(\Omega,\mathcal{F},P,d,X)$ be the formula

$$\begin{aligned} &\Pi(\Omega,\mathcal{F},P)\wedge d\in\mathbb{N}\wedge\exists c\,\bigl(c=[d]\wedge\Phi_{c}(X)\bigr)\wedge\forall t\,\forall y\,\bigl((t\in[d]\wedge(t,y)\in X)\Rightarrow\rho(\Omega,\mathcal{F},P,y)\bigr)\\ &\quad\wedge\exists v\,\Bigl(\forall\omega\,\forall h\,\forall t\,\forall y\,\forall g\,\bigl(((\omega,h)\in v\wedge t\in[d]\wedge(t,y)\in X\wedge(\omega,g)\in y)\Rightarrow(t,g)\in h\bigr)\wedge G(\Omega,\mathcal{F},P,d,v)\Bigr). \end{aligned}$$

Let sets be assigned to $x_{0},\dots,x_{4}$. The first four conjuncts hold if and only if $(\Omega,\mathcal{F},P)$ is a probability space, $d\in\mathbb{N}$ and $X=(X_{t})_{t\in[d]}$ is a family indexed by $[d]$ in which each $X_{t}$ is a random variable; if they fail, $J$ fails together with the condition of (iii). Let them hold. For each $\omega\in\Omega$ the point $t\mapsto X_{t}(\omega)$ of $\mathbb{R}^{d}$ exists, and then so does the map $Y:\Omega\to\mathbb{R}^{d}$, $Y(\omega)=(X_{1}(\omega),\dots,X_{d}(\omega))$; $Y$ is the random vector $(X_{1},\dots,X_{d})$ in $\mathbb{R}^{d}$ of Gaussian Random Vectors and Jointly Gaussian Random Variables (iii), a random vector by Random Vectors: Coordinates, Functions, Pairs and Almost-Sure Equality (i). For a map $v:\Omega\to\mathbb{R}^{d}$, the first conjunct after $\exists v$ says $v(\omega)_{t}=X_{t}(\omega)$ for all $\omega\in\Omega$ and $t\in[d]$, that is, $v=Y$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (iii)). If the last conjunct of $J$ holds with a set $v$, then $G(\Omega,\mathcal{F},P,d,v)$ makes $v$ a random vector in $\mathbb{R}^{d}$, in particular a map $v:\Omega\to\mathbb{R}^{d}$, so $v=Y$ and $Y$ is Gaussian; conversely, if $Y$ is Gaussian, $v=Y$ satisfies it. So $J$ holds if and only if $Y$ is Gaussian, that is, if and only if $X_{1},\dots,X_{d}$ are jointly Gaussian; $J$ expresses the condition of (iii) with $\Omega,\mathcal{F},P,d,X$ at $x_{0},\dots,x_{4}$.

Gaussian random variables. Let $y'$ be a set variable not occurring in $J$, let $J(\Omega,\mathcal{F},P,1_{\mathbb{N}},y')$ be obtained from $J$ by renaming $d$ to the set variable $1_{\mathbb{N}}$ and $X$ to $y'$, and let

$$H(\Omega,\mathcal{F},P,X)=\exists y'\,\bigl(\forall w\,(w\in y'\Leftrightarrow w=(1_{\mathbb{N}},X))\wedge J(\Omega,\mathcal{F},P,1_{\mathbb{N}},y')\bigr).$$

Let sets be assigned to $\Omega,\mathcal{F},P,X$. The only set $y'$ satisfying the first conjunct after $\exists y'$ is $\{(1_{\mathbb{N}},X)\}$, the function with domain $\{1_{\mathbb{N}}\}=[1]$ and value $X$ at $1_{\mathbb{N}}$, that is, $X$ as a family of one set. By the previous paragraph, with $d$ equal to the natural number $1_{\mathbb{N}}$, $J(\Omega,\mathcal{F},P,1_{\mathbb{N}},y')$ holds for this $y'$ if and only if $(\Omega,\mathcal{F},P)$ is a probability space, $X$ is a random variable, and $X$, as a family of one random variable, is jointly Gaussian, which by Gaussian Random Vectors and Jointly Gaussian Random Variables (iii) means that $X$ is Gaussian. So $H$ expresses the condition of (iv) with $\Omega,\mathcal{F},P,X$ at $x_{0},x_{1},x_{2},x_{4}$.

Positions. Rename $x_{r}$ to $x_{i_{r}}$, simultaneously, for $r\le8$ in $\Xi$ and for $r\le4$ in $G$ and $J$, and $x_{0},x_{1},x_{2},x_{4}$ to $x_{i_{0}},x_{i_{1}},x_{i_{2}},x_{i_{3}}$ in $H$, the bound variables being first renamed away from $x_{0},\dots,x_{n-1}$. The resulting formulas are predicative and express the conditions of (i), (ii), (iii) and (iv) with the sets at the positions named there, 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 (i), applied to the formula with its abbreviations eliminated, which allows the formula renamed to contain class variables, here parameters, in pair and atomic positions; their free variables are among $x_{0},\dots,x_{n-1}$ and the parameters of the statement. Hence each of the four conditions is predicative.