Facts about Gaussian characteristic function

In this file we prove that Gaussian measures over a Banach space E are exactly those measures μ such that there exist m : E and f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ positive semidefinite (satisfying f.toBilinForm.IsPosSemidef) such that charFunDual μ L = exp (L m * I - f L L / 2). We also prove that such m and f are unique and equal to ∫ x, x ∂μ and covarianceBilinDual μ.

We also specialize these statements in the case of Hilbert spaces, with f : E →L[ℝ] E →L[ℝ] ℝ, charFun μ t = exp (⟪t, m⟫ * I - f t t / 2) and f = covarianceBilin μ.

Main statements

• isGaussian_iff_gaussian_charFunDual μ: the measure μ is Gaussian if and only if there exist m : E and f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ satisfying f.toBilinForm.IsPosSemidef and charFunDual μ L = exp (L m * I - f L L / 2).
• isGaussian_iff_gaussian_charFun μ: the measure μ is Gaussian if and only if there exist m : E and f : E →L[ℝ] E →L[ℝ] ℝ satisfying f.toBilinForm.IsPosSemidef and charFun μ t = exp (⟪t, m⟫ * I - f t t / 2).

Tags

Gaussian measure, characteristic function

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

theorem ProbabilityTheory.isGaussian_iff_gaussian_charFunDual {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] : IsGaussian μ ↔ ∃ (m : E) (f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ), f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), MeasureTheory.charFunDual μ L = Complex.exp (↑(L m) * Complex.I - ↑((f L) L) / 2)

The measure μ is Gaussian if and only if there exist m : E and f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ satisfying f.toBilinForm.IsPosSemidef and charFunDual μ L = exp (L m * I - f L L / 2).

theorem ProbabilityTheory.gaussian_charFunDual_congr {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] {m : E} {f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ} (hf : f.toBilinForm.IsPosSemidef) (h : ∀ (L : StrongDual ℝ E), MeasureTheory.charFunDual μ L = Complex.exp (↑(L m) * Complex.I - ↑((f L) L) / 2)) : m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ

theorem ProbabilityTheory.IsGaussian.ext_covarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] {ν : MeasureTheory.Measure E} [IsGaussian μ] [IsGaussian ν] (hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν) (hv : covarianceBilinDual μ = covarianceBilinDual ν) : μ = ν

Two Gaussian measures are equal if they have same mean and same covariance.

theorem ProbabilityTheory.IsGaussian.ext_iff_covarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] {ν : MeasureTheory.Measure E} [IsGaussian μ] [IsGaussian ν] : μ = ν ↔ ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν ∧ covarianceBilinDual μ = covarianceBilinDual ν

Two Gaussian measures are equal if and only if they have same mean and same covariance.

theorem ProbabilityTheory.IsGaussian.charFun_eq' {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [InnerProductSpace ℝ E] [IsGaussian μ] (t : E) : MeasureTheory.charFun μ t = Complex.exp (↑(inner ℝ t (∫ (x : E), id x ∂μ)) * Complex.I - ↑(((covarianceBilin μ) t) t) / 2)

theorem ProbabilityTheory.isGaussian_iff_gaussian_charFun {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [InnerProductSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] : IsGaussian μ ↔ ∃ (m : E) (f : E →L[ℝ] E →L[ℝ] ℝ), f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), MeasureTheory.charFun μ t = Complex.exp (↑(inner ℝ t m) * Complex.I - ↑((f t) t) / 2)

The measure μ is Gaussian if and only if there exist m : E and f : E →L[ℝ] E →L[ℝ] ℝ satisfying f.toBilinForm.IsPosSemidef and charFun μ t = exp (⟪t, m⟫ * I - f t t / 2).

theorem ProbabilityTheory.gaussian_charFun_congr {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [InnerProductSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] (m : E) (f : E →L[ℝ] E →L[ℝ] ℝ) (hf : f.toBilinForm.IsPosSemidef) (h : ∀ (t : E), MeasureTheory.charFun μ t = Complex.exp (↑(inner ℝ t m) * Complex.I - ↑((f t) t) / 2)) : m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ

If the characteristic function of μ takes the form of a gaussian characteristic function, then the parameters have to be the expectation and the covariance bilinear form.

theorem ProbabilityTheory.IsGaussian.ext {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [InnerProductSpace ℝ E] {ν : MeasureTheory.Measure E} [IsGaussian μ] [IsGaussian ν] (hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν) (hv : covarianceBilin μ = covarianceBilin ν) : μ = ν

Two Gaussian measures are equal if they have same mean and same covariance. This is IsGaussian.ext_covarianceBilinDual specialized to Hilbert spaces.

theorem ProbabilityTheory.IsGaussian.ext_iff {E : Type u_1} [NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [InnerProductSpace ℝ E] {ν : MeasureTheory.Measure E} [IsGaussian μ] [IsGaussian ν] : μ = ν ↔ ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν ∧ covarianceBilin μ = covarianceBilin ν

Two Gaussian measures are equal if and only if they have same mean and same covariance. This is IsGaussian.ext_iff_covarianceBilinDual specialized to Hilbert spaces.