3 Gaussian distributions
3.1 Gaussian measures
3.1.1 Real Gaussian measures
The characteristic function of a real Gaussian measure with mean \(\mu \) and variance \(\sigma ^2\) is given by \(x \mapsto \exp \left(i \mu x - \frac{\sigma ^2 x^2}{2}\right)\).
3.1.2 Gaussian measures on a Banach space
That kind of generality is not needed for this project, but we happen to have results about Gaussian measures on a Banach space in Mathlib, so we will use them.
Let \(F\) be a separable Banach space.
A measure \(\mu \) on \(F\) is Gaussian if for every continuous linear form \(L \in F^*\), the pushforward measure \(L_* \mu \) is a Gaussian measure on \(\mathbb {R}\).
A Gaussian measure is a probability measure.
A measure \(\mu \) on \(F\) is centered if for every continuous linear form \(L \in F^*\), \(\mu [L] = 0\).
A finite measure \(\mu \) on \(F\) is Gaussian if and only if for every continuous linear form \(L \in F^*\), the characteristic function of \(\mu \) at \(L\) is
in which \(\mathbb {V}_\mu [L]\) is the variance of \(L\) with respect to \(\mu \).
Let \(\mu \) be a finite measure on \(F\) such that \(\mu \times \mu \) is invariant under the rotation of angle \(-\frac{\pi }{4}\). Then there exists \(C {\gt} 0\) such that the function \(x \mapsto \exp (C \Vert x \Vert ^2)\) is integrable with respect to \(\mu \).
For a Gaussian measure, there exists \(C {\gt} 0\) such that the function \(x \mapsto \exp (C \Vert x \Vert ^2)\) is integrable.
A Gaussian measure \(\mu \) has finite moments of all orders. In particular, there is a well defined mean \(m_\mu := \mu [\mathrm{id}]\), and for all \(L \in F^*\), \(\mu [L] = L(m_\mu )\).
The covariance bilinear form of a measure \(\mu \) with finite second moment is the continuous bilinear form \(C_\mu : F^* \times F^* \to \mathbb {R}\) with
A Gaussian measure has finite second moment by Lemma 3.9, hence its covariance bilinear form is well defined.
For \(\mu \) a measure on \(F\) with finite second moment and \(L \in F^*\), \(C_\mu (L, L) = \mathbb {V}_\mu [L]\).
Transformations of Gaussian measures
Let \(F, G\) be two Banach spaces, let \(\mu \) be a Gaussian measure on \(F\) and let \(T : F \to G\) be a continuous linear map. Then \(T_*\mu \) is a Gaussian measure on \(G\).
Let \(\mu \) be a Gaussian measure on \(F\) and let \(c \in F\). Then the measure \(\mu \) translated by \(c\) (the map of \(\mu \) by \(x \mapsto x + c\)) is a Gaussian measure on \(F\).
The convolution of two Gaussian measures is a Gaussian measure.
3.1.3 Gaussian measures on a finite dimensional Hilbert space
A finite measure \(\mu \) on a separable Hilbert space \(E\) is Gaussian if and only if for every \(t \in E\), the characteristic function of \(\mu \) at \(t\) is
By Theorem 3.6, \(\mu \) is Gaussian iff for every continuous linear form \(L \in E^*\), the characteristic function of \(\mu \) at \(L\) is
Every continuous linear form \(L \in E^*\) can be written as \(L(x) = \langle t, x \rangle \) for some \(t \in E\), hence we have that \(\mu \) is Gaussian iff for every \(t \in E\),
Let \(E\) be a finite dimensional Hilbert space. We denote by \(\langle \cdot , \cdot \rangle \) the inner product on \(E\) and by \(\Vert \cdot \Vert \) the associated norm.
The covariance matrix of a Gaussian measure \(\mu \) on \(E\) is the positive semidefinite matrix \(\Sigma _\mu \) with
The characteristic function of a Gaussian measure \(\mu \) on \(E\) is given by
By Lemma 3.15, for every \(t \in E\),
By Lemma 3.9, \(\mu \) has finite first moment and \(\mu [\langle t, \cdot \rangle ] = \langle t, m_\mu \rangle \).
TODO: the second moment is also finite and we can get to the covariance matrix.
A finite measure \(\mu \) on \(E\) is Gaussian if and only if there exists \(m \in E\) and \(\Sigma \) positive semidefinite such that for all \(t \in E\), the characteristic function of \(\mu \) at \(t\) is
If that’s the case, then \(m = m_\mu \) and \(\Sigma = \Sigma _\mu \).
Note that this lemma does not say that there exists a Gaussian measure for any such \(m\) and \(\Sigma \). We will prove that later.
Lemma 3.17 states that the characteristic function of a Gaussian measure has the wanted form.
Suppose now that there exists \(m \in E\) and \(\Sigma \) positive semidefinite such that for all \(t \in E\), \(\hat{\mu }(t) = \exp \left(i \langle t, m \rangle - \frac{1}{2} \langle t, \Sigma t \rangle \right)\).
We need to show that for all \(L \in E^*\), \(L_*\mu \) is a Gaussian measure on \(\mathbb {R}\). Such an \(L\) can be written as \(\langle u, \cdot \rangle \) for some \(u \in E\). Let then \(u \in E\). We compute the characteristic function of \(\langle u, \cdot \rangle _*\mu \) at \(x \in \mathbb {R}\) with Lemma 2.5:
This is the characteristic function of a Gaussian measure on \(\mathbb {R}\) with mean \(\langle u, m \rangle \) and variance \(\langle u, \Sigma u \rangle \). By Theorem 2.4, \(\langle u, \cdot \rangle _*\mu \) is Gaussian, hence \(\mu \) is Gaussian.
Let \((e_1, \ldots , e_d)\) be an orthonormal basis of \(E\) and let \(\mu _1, \ldots , \mu _d\) be independent standard Gaussian measures on \(\mathbb {R}\). The standard Gaussian measure on \(E\) is the pushforward measure of the product measure \(\mu _1 \times \ldots \times \mu _d\) by the map \(x \mapsto \sum _{i=1}^d x_i \cdot e_i\).
The standard Gaussian measure on \(E\) is centered, i.e., \(\mu [L] = 0\) for every \(L \in E^*\).
THe standard Gaussian measure is a probability measure.
The characteristic function of the standard Gaussian measure on \(E\) is given by
The standard Gaussian measure on \(E\) is a Gaussian measure.
The multivariate Gaussian measure on \(\mathbb {R}^d\) with mean \(m \in \mathbb {R}^d\) and covariance matrix \(\Sigma \in \mathbb {R}^{d \times d}\), with \(\Sigma \) positive semidefinite, is the pushforward measure of the standard Gaussian measure on \(\mathbb {R}^d\) by the map \(x \mapsto m + \Sigma ^{1/2} x\). We denote this measure by \(\mathcal{N}(m, \Sigma )\).
The characteristic function of a multivariate Gaussian measure \(\mathcal{N}(m, \Sigma )\) is given by
A multivariate Gaussian measure is a Gaussian measure.
3.2 Gaussian processes
A process \(X : T \to \Omega \to E\) is Gaussian if for every finite subset \(t_1, \ldots , t_n \in T\), the random vector \((X_{t_1}, \ldots , X_{t_n})\) has a Gaussian distribution.