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]

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

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.

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.

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

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.

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.

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 μ

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) μ

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 μ

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 μ

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 ∂μ)

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.

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.

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.

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.