Facts about Gaussian characteristic function

instance ProbabilityTheory.IsGaussian.isProbabilityMeasure {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.

theorem ProbabilityTheory.isGaussian_iff_charFun_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure 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)

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

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

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

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] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [SecondCountableTopology E] {ν : MeasureTheory.Measure E} [IsGaussian μ] [IsGaussian ν] (hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν) (hv : covInnerBilin μ = covInnerBilin ν) : μ = ν

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

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

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

theorem ProbabilityTheory.IsGaussian.ext_covarianceBilin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace 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.

theorem ProbabilityTheory.IsGaussian.ext_iff_covarianceBilin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace 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.