How to define the Gaussian measure

Stream: maths

[Jason KY.]

I think it would be nice to define the Gaussian measure sometime soon as it is important for the CLT and Brownian motions but it is not clear to me what is the best way of doing it. In particular, I would like Gaussian to be a predicate on the space measures on topological vector spaces and allow for degenerate Gaussians.

Here is what I'm thinking and how we might define it:
(1) A random variable $f : \Omega \to \mathbb{R}$ is standard Gaussian (on $(\Omega, \mathcal{F}, \mathbb{P})$) if $f_* \mathbb{P} = (2\pi)^{-1/2} e^{-x^2/2}\lambda$.

(2) A random variable $f : \Omega \to \mathbb{R}$ is Gaussian if there exists some $s, m \in \mathbb{R}$ such that $f = sg + m$ where $g$ is a standard Gaussian.

(3) A measure $\mu$ on $\mathbb{R}$ is Gaussian if there exists some measure space $(\Omega, \mathcal{F}, \mathbb{P})$ such that $\mu = f_* \mathbb{P}$ where $f$ is a Gaussian.

(4) If $E$ is some space such that $E^*$ makes sense then a measure $\mu$ on $E$ is Gaussian if for all $l \in E^*$, $l_* \mu$ is a Gaussian measure on $\mathbb{R}$ .

I'm personally not very happy with step 3 since we need to choose a measure space. Is there a better way of defining the Gaussian that I'm overlooking?

[Oliver Nash]

I presume you've looked at https://mathoverflow.net/questions/407465/definition-of-infinite-dimensional-gaussian-random-variable

[Oliver Nash]

It looks to me like this provide a convenient alternative to your (3).

[Jason KY.]

Ah yes. I completely forgot about that mathoverflow page. Thanks!

[Oliver Nash]

I remember it because the answer was blessed by Hairer himself!

[Sebastien Gouezel]

First you should define the Gaussian measure with mean $c$ and variance $\sigma^2$ on the real line, as the measure with a density $\frac{1}{\sqrt{2\pi\sigma^2}}e^{-(x-c)^2/(2 sigma^2)}$ (you will need #15106 to check that this a probability measure). Then, to say that a real-valued random variable is Gaussian you look at the image measure.

[Jason KY.]

But this definition wouldn't allow the degenerate Gaussian measure to be a Gaussian measure right?

[Kalle Kytölä]

I guess all agree (as Sébastien explicitly said) that a gaussian random variable is a random variable whose distribution, i.e., the pushed-forward underlying probability measure to $\R$, is a gaussian measure on $\R$. And gaussianity in more general vector spaces than $\R$ is reduced to the case of $\R$ (like in the linked Stack Exchange discussion).

So I interpret Jason's question as: "how do we define the gaussian measures on $\R$?"

I'd have no qualms about a definition by density, if it wasn't for degenerate cases (a gaussian of zero variance has no density!). The degenerate cases should be considered gaussian (otherwise the reduction of more general gaussians to real gaussians doesn't work). In fact degenerate gaussians become even more important in more than 1-dimensional case, since gaussians are often supported on proper subspaces (and are thus degenerate in some directions). (E.g., the 2D gaussian free field on essentially Sobolev-regularity $-1/2$ subspace of whatever space you a priori build it in.)

For this reason I'd much prefer the definition by characteristic functions to the definition by densities --- no ad hoc treatment of the $\sigma^2 = 0$ case would be needed. (And moreover, the characteristic function is anyway how calculations with gaussians are done.)

Of course we don't have characteristic functions yet, so this is not feasible in short term. Good enough Fourier analysis would probably be needed for characteristic functions, since the mathlib approach would not be to do the Fourier transforms of finite measures on the real line separately from the Fourier transforms of distributions, say.

Jason's "shift and scale a standard Gaussian" is a way to circumvent the problem of degenerate Gaussians in dimension one. I think it is better than the "only density" definition in that it includes the degenerate case and one can therefore safely build multidimensional gaussians and gaussian processes on that definition. But in my opinion it is not as elegant as the characteristic function definition...

[Sebastien Gouezel]

If you want a Dirac mass to be Gaussian (this depends on the conventions), then you can allow it if you like and define the Gaussian measure with mean $c$ and variance $0$ to be the Dirac mass at $c$.

[Sebastien Gouezel]

Fourier transform is something complicated to implement cleanly, as there are a lot of different natural settings (finite measures, distributions, integrable functions, functions in the Schwartz class) where the Fourier transform lives in different spaces (functions, distributions, functions in the Schwarz class, and so on). So I wouldn't oppose an ad hoc definition of characteristic functions and building a minimal API (up to the Lévy convergence theorem, say), independently of a more general theory.

[Jason KY.]

Sure, that works!

[Oliver Nash]

Earlier today @Kevin Buzzard asked me if we had the definition of Gaussian measures yet.

It looks like @Jason KY. showed us how to do it last year (I've tweaked his code and translated to Lean 4, any mistakes are likely mine):

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

-- Based on Jason's work:
-- https://github.com/leanprover-community/mathlib/commit/b7048541b780ba86f8643f339309adb96eb0f5fe
-- https://github.com/leanprover-community/mathlib/commit/fbe2eeeaa939e56fa904f19c63f81a36eee12b29

open ENNReal NNReal Real

noncomputable section

namespace MeasureTheory.Measure

def gaussianDensity (m s x : ℝ) : ℝ≥0∞ :=
  ENNReal.ofReal <| (s * sqrt (2 * π))⁻¹ * exp (- 2⁻¹ * ((x - m) / s) ^ 2)

def realGaussian (m s : ℝ) :=
  if s = 0 then dirac m else volume.withDensity (gaussianDensity m s)

-- Data: we need these
variable {E : Type*}
  [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [MeasurableSpace E] (ν : Measure E)

-- Props: should some / all of these be included?
variable [ContinuousAdd E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [BorelSpace E]
  [IsLocallyFiniteMeasure ν] [OuterRegular ν] (hν : InnerRegular ν IsCompact IsOpen)

def isGaussian : Prop :=
  ∀ l : E →L[ℝ] ℝ, ∃ m s, ν.map l = realGaussian m s

end MeasureTheory.Measure

[Oliver Nash]

But there was a question of whether we could instead use characteristic functions.

So I wonder: how far away are we from having characteristic functions? Maybe @Rémy Degenne has some idea?

[Jason KY.]

FYI, @Rémy Degenne has a repo defining the real gaussian here

[Rémy Degenne]

The real case was also done very similarly to what you just wrote by @Lorenzo Luccioli at lftcm. But it has not been PRed to mathlib (it's here: https://github.com/RemyDegenne/gaussian/blob/master/Gaussian/Gaussian.lean).
We are not far away from having characteristic functions. @Jason KY., @Peter Pfaffelhuber and I are working on that and we will add those very soon.

[Rémy Degenne]

And even if we don't have a Gaussian measure definition in mathlib, we already have computations related to it, like docs#fourier_transform_gaussian

[Oliver Nash]

Wow, this is all great news. Thanks!

[Vincent Beffara]

Is the plan to define the real valued Gaussian, and then to say that a measure is Gaussian iff it is mapped to a real Gaussian by any linear form? Ah sorry I should have read the code before asking ...

[Oliver Nash]

It's good to ask: the code is just one possibility, and questions like this https://mathoverflow.net/questions/123493/what-is-a-gaussian-measure suggest we could consider alternatives (though I'm not fit to judge).