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

source
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

Instances

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

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

A real Gaussian measure is Gaussian.

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

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

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

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

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

source
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 ν)
source
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) μ)
source
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) μ)
source
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) μ)
source
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) μ)
source
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) μ)
source
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.