# 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 exists `C > 0` such that the function `x ↦ 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 #

- [Martin Hairer, An introduction to stochastic PDEs][hairer2009introduction]

source
theorem ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] (hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0) (L : StrongDual ℝ E) :
MeasureTheory.charFunDual μ L = Complex.exp (-↑(variance (⇑L) μ) / 2)

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`

source
theorem ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [SecondCountableTopology E] [CompleteSpace E] (hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0) (θ : ℝ) :
MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ) = μ.prod μ

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`.

source
theorem ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [SecondCountableTopology E] (L : StrongDual ℝ E) :
∫ (x : E), L x ∂μ.conv (MeasureTheory.Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) = 0

The convolution of a Gaussian measure `μ` and its map by `x ↦ -x` is centered.

source
theorem ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [IsGaussian μ] {C C' : ℝ} (hint : MeasureTheory.Integrable (fun (x : E) => Real.exp (C * ‖x‖ ^ 2)) (μ.conv (MeasureTheory.Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ))) (hC'_pos : 0 < C') (hC'_lt : C' < C) :
MeasureTheory.Integrable (fun (x : E) => Real.exp (C' * ‖x‖ ^ 2)) μ

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 `μ`.

source
theorem ProbabilityTheory.IsGaussian.exists_integrable_exp_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [IsGaussian μ] :
∃ (C : ℝ), 0 < C ∧ MeasureTheory.Integrable (fun (x : E) => Real.exp (C * ‖x‖ ^ 2)) μ

Fernique's theorem: for a Gaussian measure, there exists `C > 0` such that the function `x ↦ exp (C * ‖x‖ ^ 2)` is integrable.

source
theorem ProbabilityTheory.IsGaussian.memLp_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [IsGaussian μ] (p : ENNReal) (hp : p ≠ ⊤) :
MeasureTheory.MemLp id p μ

A Gaussian measure has moments of all orders. That is, the identity is in L^p for all finite `p`.

source
theorem ProbabilityTheory.IsGaussian.integrable_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] :
MeasureTheory.Integrable id μ
source
theorem ProbabilityTheory.IsGaussian.integrable_fun_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] :
MeasureTheory.Integrable (fun (x : E) => x) μ
source
theorem ProbabilityTheory.IsGaussian.memLp_two_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] :
MeasureTheory.MemLp id 2 μ
source
theorem ProbabilityTheory.IsGaussian.memLp_two_fun_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] :
MeasureTheory.MemLp (fun (x : E) => x) 2 μ
source
theorem ProbabilityTheory.IsGaussian.integral_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (L : StrongDual ℝ E) :
∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
source
theorem ProbabilityTheory.IsGaussian.eq_dirac_of_variance_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (h : ∀ (L : StrongDual ℝ E), variance (⇑L) μ = 0) :
μ = MeasureTheory.Measure.dirac (∫ (x : E), x ∂μ)

A Gaussian measure with variance zero is a Dirac.

source
theorem ProbabilityTheory.IsGaussian.noAtoms {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (h : ∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x) :
MeasureTheory.NoAtoms μ

If a Gaussian measure is not a Dirac, then it has no atoms.

source
theorem ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (hμ : ∫ (x : E), id x ∂μ = 0) (L : StrongDual ℝ E) :
MeasureTheory.charFunDual μ L = Complex.exp (-↑(variance (⇑L) μ) / 2)

Characteristic function of a centered Gaussian measure.

source
theorem ProbabilityTheory.IsGaussian.map_rotation_eq_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (hμ : ∫ (x : E), id x ∂μ = 0) (θ : ℝ) :
MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ) = μ.prod μ

For a centered Gaussian measure `μ`, the product measure `μ.prod μ` is invariant under rotation.