Gaussian distributions in Banach spaces

We introduce a predicate IsGaussian for measures on a Banach space E such that the map by any continuous linear form is a Gaussian measure on ℝ.

For Gaussian distributions in ℝ, see the file Mathlib.Probability.Distributions.Gaussian.Real.

Main definitions

• IsGaussian: a measure μ is Gaussian if its map by every continuous linear form L : Dual ℝ E is a real Gaussian measure. That is, μ.map L = gaussianReal (μ[L]) (Var[L; μ]).toNNReal.

Main statements

• isGaussian_iff_charFunDual_eq: a finite measure μ is Gaussian if and only if its characteristic function has value exp (μ[L] * I - Var[L; μ] / 2) for every continuous linear form L : Dual ℝ E.

References

• Martin Hairer, An introduction to stochastic PDEs

class ProbabilityTheory.IsGaussian {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {mE : MeasurableSpace E} (μ : MeasureTheory.Measure E) : Prop

A measure is Gaussian if its map by every continuous linear form is a real Gaussian measure.

• map_eq_gaussianReal (L : StrongDual ℝ E) : MeasureTheory.Measure.map (⇑L) μ = gaussianReal (∫ (x : E), L x ∂μ) (variance (⇑L) μ).toNNReal

instance ProbabilityTheory.IsGaussian.toIsProbabilityMeasure {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {mE : MeasurableSpace E} (μ : MeasureTheory.Measure E) [IsGaussian μ] : MeasureTheory.IsProbabilityMeasure μ

A Gaussian measure is a probability measure.

instance ProbabilityTheory.isGaussian_gaussianReal (m : ℝ) (v : NNReal) : IsGaussian (gaussianReal m v)

A real Gaussian measure is Gaussian.

theorem ProbabilityTheory.IsGaussian.eq_gaussianReal (μ : MeasureTheory.Measure ℝ) (h : IsGaussian μ) : μ = gaussianReal (∫ (x : ℝ), id x ∂μ) (variance id μ).toNNReal

A Gaussian measure over ℝ is some gaussianReal.

theorem ProbabilityTheory.isGaussian_of_isGaussian_map {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} (h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (MeasureTheory.Measure.map (⇑L) μ)) : IsGaussian μ

theorem ProbabilityTheory.isGaussian_of_map_eq_gaussianReal {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} (h : ∀ (L : E →L[ℝ] ℝ), ∃ (m : ℝ) (v : NNReal), MeasureTheory.Measure.map (⇑L) μ = gaussianReal m v) : IsGaussian μ

instance ProbabilityTheory.instIsGaussianDirac {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {x : E} : IsGaussian (MeasureTheory.Measure.dirac x)

Dirac measures are Gaussian.

theorem ProbabilityTheory.IsGaussian.memLp_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [IsGaussian μ] (L : StrongDual ℝ E) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (⇑L) p μ

theorem ProbabilityTheory.IsGaussian.integrable_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [IsGaussian μ] (L : StrongDual ℝ E) : MeasureTheory.Integrable (⇑L) μ

instance ProbabilityTheory.isGaussian_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {μ : MeasureTheory.Measure E} [IsGaussian μ] (L : E →L[ℝ] F) : IsGaussian (MeasureTheory.Measure.map (⇑L) μ)

The map of a Gaussian measure by a continuous linear map is Gaussian.

instance ProbabilityTheory.isGaussian_map_equiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {μ : MeasureTheory.Measure E} [IsGaussian μ] (L : E ≃L[ℝ] F) : IsGaussian (MeasureTheory.Measure.map (⇑L) μ)

theorem ProbabilityTheory.isGaussian_map_equiv_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {μ : MeasureTheory.Measure E} (L : E ≃L[ℝ] F) : IsGaussian (MeasureTheory.Measure.map (⇑L) μ) ↔ IsGaussian μ

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

The characteristic function of a Gaussian measure μ has value exp (μ[L] * I - Var[L; μ] / 2) at L : Dual ℝ E.

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

A finite measure is Gaussian iff its characteristic function has value exp (μ[L] * I - Var[L; μ] / 2) for every L : Dual ℝ E.

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

Alias of the reverse direction of ProbabilityTheory.isGaussian_iff_charFunDual_eq.

---

A finite measure is Gaussian iff its characteristic function has value exp (μ[L] * I - Var[L; μ] / 2) for every L : Dual ℝ E.

theorem ProbabilityTheory.IsGaussian.charFun_eq {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] (t : E) : MeasureTheory.charFun μ t = Complex.exp ((∫ (x : E), ↑((fun (x : E) => inner ℝ t x) x) ∂μ) * Complex.I - ↑(variance (fun (x : E) => inner ℝ t x) μ) / 2)

theorem ProbabilityTheory.isGaussian_iff_charFun_eq {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] : IsGaussian μ ↔ ∀ (t : E), MeasureTheory.charFun μ t = Complex.exp ((∫ (x : E), ↑((fun (x : E) => inner ℝ t x) x) ∂μ) * Complex.I - ↑(variance (fun (x : E) => inner ℝ t x) μ) / 2)

instance ProbabilityTheory.isGaussian_conv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ ν : MeasureTheory.Measure E} [IsGaussian μ] [IsGaussian ν] : IsGaussian (μ.conv ν)

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

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

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

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

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

instance ProbabilityTheory.instIsGaussianProdProdOfSecondCountableTopologyEither {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {μ : MeasureTheory.Measure E} [IsGaussian μ] [SecondCountableTopologyEither E F] {ν : MeasureTheory.Measure F} [IsGaussian ν] : IsGaussian (μ.prod ν)

A product of Gaussian distributions is Gaussian.