Multivariate Gaussian distributions

In this file we define the standard Gaussian distribution over a Euclidean space and multivariate Gaussian distributions over EuclideanSpace ℝ ι.

Main definitions

• stdGaussian E: Standard Gaussian distribution on a finite-dimensional real inner product space E. This is the random vector whose coordinates in an orthonormal basis are independent standard Gaussian.
• multivariateGaussian μ S: The multivariate Gaussian distribution on EuclideanSpace ℝ ι with mean μ and covariance matrix S, when S is a positive semidefinite matrix.

TODO

• Generalize multivariateGaussian μ S when S is a symmetric trace class operator over a Hilbert space.

Tags

multivariate Gaussian distribution

Standard Gaussian measure over a Euclidean space

noncomputable def ProbabilityTheory.stdGaussian (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] : MeasureTheory.Measure E

Standard Gaussian distribution on a finite-dimensional real inner product space E. This is the random vector whose coordinates in an orthonormal basis are independent standard Gaussian.

The definition uses stdOrthonormalBasis ℝ E but does not actually depend on the basis, see stdGaussian_eq_map_pi_orthonormalBasis.

Equations

• One or more equations did not get rendered due to their size.

instance ProbabilityTheory.isProbabilityMeasure_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.IsProbabilityMeasure (stdGaussian E)

@[simp]

theorem ProbabilityTheory.integral_id_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ∫ (x : E), x ∂stdGaussian E = 0

theorem ProbabilityTheory.variance_dual_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : StrongDual ℝ E) : variance (⇑L) (stdGaussian E) = ‖L‖ ^ 2

theorem ProbabilityTheory.charFun_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (t : E) : MeasureTheory.charFun (stdGaussian E) t = Complex.exp (-↑‖t‖ ^ 2 / 2)

instance ProbabilityTheory.isGaussian_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : IsGaussian (stdGaussian E)

@[simp]

theorem ProbabilityTheory.integral_strongDual_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : StrongDual ℝ E) : ∫ (x : E), L x ∂stdGaussian E = 0

theorem ProbabilityTheory.charFunDual_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : StrongDual ℝ E) : MeasureTheory.charFunDual (stdGaussian E) L = Complex.exp (-↑‖L‖ ^ 2 / 2)

theorem ProbabilityTheory.covarianceBilin_stdGaussian {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : covarianceBilin (stdGaussian E) = innerSL ℝ

theorem ProbabilityTheory.stdGaussian_map {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (f : E ≃ₗᵢ[ℝ] F) : MeasureTheory.Measure.map (⇑f) (stdGaussian E) = stdGaussian F

theorem ProbabilityTheory.map_pi_eq_stdGaussian {ι : Type u_1} [Fintype ι] : MeasureTheory.Measure.map (WithLp.toLp 2) (MeasureTheory.Measure.pi fun (x : ι) => gaussianReal 0 1) = stdGaussian (EuclideanSpace ℝ ι)

theorem ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (b : OrthonormalBasis ι ℝ E) : stdGaussian E = MeasureTheory.Measure.map (fun (x : ι → ℝ) => ∑ i : ι, x i • b i) (MeasureTheory.Measure.pi fun (x : ι) => gaussianReal 0 1)

The definition of stdGaussian does not depend on the basis.

Multivariate Gaussian measures over ℝⁿ

noncomputable def ProbabilityTheory.multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) : MeasureTheory.Measure (EuclideanSpace ℝ ι)

Multivariate Gaussian measure on EuclideanSpace ℝ ι with mean μ and covariance matrix S. This only makes sense when S is positive semidefinite, as then CFC.sqrt S * CFC.sqrt S = S. Otherwise CFC.sqrt S = 0, and multivariateGaussian μ S = Measure.dirac μ (see multivariateGaussian_of_not_posSemidef).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.multivariateGaussian_of_not_posSemidef {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : ¬S.PosSemidef) : multivariateGaussian μ S = MeasureTheory.Measure.dirac μ

@[simp]

theorem ProbabilityTheory.multivariateGaussian_zero_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] : multivariateGaussian 0 1 = stdGaussian (EuclideanSpace ℝ ι)

instance ProbabilityTheory.isGaussian_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} : IsGaussian (multivariateGaussian μ S)

@[simp]

theorem ProbabilityTheory.integral_id_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} : ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ

theorem ProbabilityTheory.integral_id_multivariateGaussian' {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} : ∫ (x : EuclideanSpace ℝ ι), id x ∂multivariateGaussian μ S = μ

theorem ProbabilityTheory.covarianceBilin_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (x y : EuclideanSpace ℝ ι) : ((covarianceBilin (multivariateGaussian μ S)) x) y = x.ofLp ⬝ᵥ S.mulVec y.ofLp

theorem ProbabilityTheory.covariance_eval_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (i j : ι) : covariance (fun (x : EuclideanSpace ℝ ι) => x.ofLp i) (fun (x : EuclideanSpace ℝ ι) => x.ofLp j) (multivariateGaussian μ S) = S i j

theorem ProbabilityTheory.variance_eval_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (i : ι) : variance (fun (x : EuclideanSpace ℝ ι) => x.ofLp i) (multivariateGaussian μ S) = S i i

theorem ProbabilityTheory.measurePreserving_eval_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} (hS : S.PosSemidef) {i : ι} : MeasureTheory.MeasurePreserving (fun (x : EuclideanSpace ℝ ι) => x.ofLp i) (multivariateGaussian μ S) (gaussianReal (μ.ofLp i) (S i i).toNNReal)

theorem ProbabilityTheory.charFun_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (x : EuclideanSpace ℝ ι) : MeasureTheory.charFun (multivariateGaussian μ S) x = Complex.exp (↑(inner ℝ x μ) * Complex.I - ↑(x.ofLp ⬝ᵥ S.mulVec x.ofLp) / 2)

theorem ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian {ι : Type u_2} [DecidableEq ι] {I J : Finset ι} {μ : EuclideanSpace ℝ ↥I} {S : Matrix ↥I ↥I ℝ} (hS : S.PosSemidef) (hJI : J ⊆ I) : MeasureTheory.MeasurePreserving (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S) (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ) (S.submatrix (fun (i : ↥J) => ⟨↑i, ⋯⟩) fun (i : ↥J) => ⟨↑i, ⋯⟩))

If one restricts a multivariate Gaussian measure indexed by a finite set I to coordinates indexed by J ⊆ I, one obtains the multivariate Gaussian measure whose covariance matrix is given by the corresponding submatrix.