Facts about Gaussian characteristic function

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.HasGaussianLaw.charFun_toLp {ι : Type u_2} {Ω : Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {X : ι → Ω → ℝ} [hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P] (ξ : EuclideanSpace ℝ ι) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) P) ξ = Complex.exp (∑ i : ι, (↑(ξ i) * ∫ (x : Ω), ↑(X i x) ∂P) * Complex.I - ∑ i : ι, ∑ j : ι, ↑(ξ i) * ↑(ξ j) * (↑(covariance (X i) (X j) P) / 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.

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)