Gaussian distributions in Banach spaces: Fernique's theorem

instance ProbabilityTheory.instIsGaussianMapHAdd_brownianMotion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (c : E) : IsGaussian (MeasureTheory.Measure.map (fun (x : E) => x + c) μ)

instance ProbabilityTheory.instIsGaussianMapHAdd_brownianMotion_1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (c : E) : IsGaussian (MeasureTheory.Measure.map (fun (x : E) => c + x) μ)

instance ProbabilityTheory.instIsGaussianMapHSub_brownianMotion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (c : E) : IsGaussian (MeasureTheory.Measure.map (fun (x : E) => x - c) μ)

theorem ProbabilityTheory.IsGaussian.exists_integrable_exp_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology 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] [SecondCountableTopology E] [CompleteSpace 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 Lp for all finite p.

theorem ProbabilityTheory.IsGaussian.memLp_two_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] : MeasureTheory.MemLp id 2 μ

theorem ProbabilityTheory.IsGaussian.integrable_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] : MeasureTheory.Integrable id μ

theorem ProbabilityTheory.IsGaussian.integrable_fun_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] : MeasureTheory.Integrable (fun (x : E) => x) μ

theorem ProbabilityTheory.IsGaussian.integral_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [SecondCountableTopology E] [CompleteSpace E] (L : NormedSpace.Dual ℝ E) : ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)