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.

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][hairer2009introduction]

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 : E →L[ℝ] ℝ) : MeasureTheory.Measure.map (⇑L) μ = gaussianReal (∫ (x : E), L x ∂μ) (variance (⇑L) μ).toNNReal

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

A real Gaussian measure is Gaussian.

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.

instance ProbabilityTheory.instIsProbabilityMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] : MeasureTheory.IsProbabilityMeasure μ

A Gaussian measure is a probability measure.

theorem ProbabilityTheory.IsGaussian.memLp_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [IsGaussian μ] (L : NormedSpace.Dual ℝ 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 : NormedSpace.Dual ℝ 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 : NormedSpace.Dual ℝ 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 : NormedSpace.Dual ℝ 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 : NormedSpace.Dual ℝ 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.