Fernique's theorem for Gaussian measures #
We show that the product of two identical Gaussian measures is invariant under rotation.
We then deduce Fernique's theorem, which states that for a Gaussian measure μ, there exists
C > 0 such that the function x ↦ exp (C * ‖x‖ ^ 2) is integrable with respect to μ.
As a consequence, a Gaussian measure has finite moments of all orders.
Main statements #
IsGaussian.exists_integrable_exp_sq: Fernique's theorem. For a Gaussian measure on a second-countable normed space, there existsC > 0such that the functionx ↦ exp (C * ‖x‖ ^ 2)is integrable.IsGaussian.memLp_id: a Gaussian measure in a second-countable Banach space has finite moments of all orders.
References #
Characteristic function of a centered Gaussian measure.
For a Gaussian measure, the hypothesis ∀ L : StrongDual ℝ E, μ[L] = 0 is equivalent to the simpler
μ[id] = 0, but at this point we don't know yet that μ has a first moment so we can't use it.
See charFunDual_eq_of_integral_eq_zero
For a centered Gaussian measure μ, the product measure μ.prod μ is invariant under rotation.
The hypothesis ∀ L : StrongDual ℝ E, μ[L] = 0 is equivalent to the simpler
μ[id] = 0, but at this point we don't know yet that μ has a first moment so we can't use it.
See map_rotation_eq_self.
The convolution of a Gaussian measure μ and its map by x ↦ -x is centered.
If x ↦ exp (C * ‖x‖ ^ 2) is integrable with respect to the centered Gaussian
μ ∗ (μ.map (ContinuousLinearEquiv.neg ℝ)), then for all C' < C, x ↦ exp (C' * ‖x‖ ^ 2)
is integrable with respect to μ.
Fernique's theorem: for a Gaussian measure, there exists C > 0 such that the function
x ↦ exp (C * ‖x‖ ^ 2) is integrable.
A Gaussian measure has moments of all orders.
That is, the identity is in L^p for all finite p.
A Gaussian measure with variance zero is a Dirac.
If a Gaussian measure is not a Dirac, then it has no atoms.
Characteristic function of a centered Gaussian measure.
For a centered Gaussian measure μ, the product measure μ.prod μ is invariant under
rotation.