Facts about Gaussian characteristic function

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

theorem ProbabilityTheory.gaussian_charFunDual_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {m : E} {f : ContinuousBilinForm ℝ (StrongDual ℝ E)} (hf : f.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] [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 : 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] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace 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_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), 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_covarianceBilinDual 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_covarianceBilinDual 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 : covarianceBilinDual μ = covarianceBilinDual ν) : μ = ν

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 ∂ν ∧ covarianceBilinDual μ = covarianceBilinDual ν

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

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

theorem ProbabilityTheory.HasGaussianLaw.map_eq_gaussianReal {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} [HasGaussianLaw X P] : MeasureTheory.Measure.map X P = gaussianReal (∫ (x : Ω), X x ∂P) (variance X P).toNNReal

theorem ProbabilityTheory.HasGaussianLaw.charFun_map_real {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} [HasGaussianLaw X P] (t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map X P) t = Complex.exp ((↑t * ∫ (x : Ω), ↑(X x) ∂P) * Complex.I - ↑t ^ 2 * ↑(variance X P) / 2)