The density of a multivariate Gaussian measure

A multivariate Gaussian law with positive-definite covariance S is Lebesgue measure on EuclideanSpace ℝ ι weighted by the classical density

(2π)^(-d/2) * (det S)^(-1/2) * exp (-⟪x - m, S⁻¹ (x - m)⟫ / 2),

where d is the dimension. Every other covariance parameter gives a law carried by a proper affine subspace, so it is singular with respect to Lebesgue measure and has no density against it.

The nondegenerate case comes from the isotropic product density (TauCeti.Probability.pi_gaussianReal_eq_withDensity) by an affine change of variables along the square root of the covariance, which contributes the Jacobian √(det S) and turns the isotropic quadratic form into the one of S⁻¹.

Main definitions

• TauCeti.Probability.multivariateGaussianPDFReal — the real-valued density;
• TauCeti.Probability.multivariateGaussianPDF — its ℝ≥0∞-valued companion.

Main results

• TauCeti.Probability.stdGaussian_eq_withDensity — the standard Gaussian on EuclideanSpace ℝ ι is Lebesgue measure weighted by (2π)^(-d/2) * exp (-‖x‖² / 2);
• TauCeti.Probability.stdGaussian_eq_withDensity_norm — the same density on any finite-dimensional real inner product space;
• TauCeti.Probability.support_multivariateGaussian — the support at a positive-semidefinite covariance is the affine range m + range S;
• TauCeti.Probability.ae_mem_affineRange_multivariateGaussian — the law is almost surely in this affine range;
• TauCeti.Probability.multivariateGaussian_eq_withDensity — the density presentation of the law;
• TauCeti.Probability.hasPDF_of_hasLaw_multivariateGaussian and TauCeti.Probability.pdf_eq_multivariateGaussianPDF_of_hasLaw_multivariateGaussian — the HasPDF bridge and the identification of MeasureTheory.pdf;
• TauCeti.Probability.rnDeriv_multivariateGaussian — the Radon–Nikodym derivative;
• TauCeti.Probability.mutuallySingular_multivariateGaussian_volume — singularity at every covariance parameter that is not positive definite.

References

• M. L. Eaton, Multivariate Statistics: A Vector Space Approach.

noncomputable def TauCeti.Probability.multivariateGaussianPDFReal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : ℝ

The density of the multivariate Gaussian law with mean m and covariance S, as a real number. It is the density of multivariateGaussian m S when S is positive definite (TauCeti.Probability.multivariateGaussian_eq_withDensity); at every other S that law has no density with respect to Lebesgue measure (TauCeti.Probability.mutuallySingular_multivariateGaussian_volume).

noncomputable def TauCeti.Probability.multivariateGaussianPDF {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : ENNReal

The ℝ≥0∞-valued companion to TauCeti.Probability.multivariateGaussianPDFReal.

theorem TauCeti.Probability.multivariateGaussianPDFReal_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) : multivariateGaussianPDFReal m S = fun (x : EuclideanSpace ℝ ι) => (2 * Real.pi) ^ (-↑(Fintype.card ι) / 2) * S.det ^ (-1 / 2) * Real.exp (-inner ℝ (x - m) ((Matrix.toEuclideanLin S⁻¹) (x - m)) / 2)

The defining formula of the real-valued density.

theorem TauCeti.Probability.multivariateGaussianPDF_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) : multivariateGaussianPDF m S = fun (x : EuclideanSpace ℝ ι) => ENNReal.ofReal (multivariateGaussianPDFReal m S x)

The ℝ≥0∞-valued density is the ENNReal.ofReal lift of the real-valued one.

theorem TauCeti.Probability.multivariateGaussianPDFReal_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hdet : 0 < S.det) (m x : EuclideanSpace ℝ ι) : 0 < multivariateGaussianPDFReal m S x

The density is positive wherever the determinant is, in particular at a positive-definite covariance, where Matrix.PosDef.det_pos supplies the hypothesis.

theorem TauCeti.Probability.multivariateGaussianPDFReal_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : 0 ≤ multivariateGaussianPDFReal m S x

The real-valued density is nonnegative at every covariance parameter. At a negative determinant the real power S.det ^ (-1/2) vanishes, so the density is 0 there.

theorem TauCeti.Probability.multivariateGaussianPDF_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hdet : 0 < S.det) (m x : EuclideanSpace ℝ ι) : 0 < multivariateGaussianPDF m S x

The ℝ≥0∞-valued density is positive wherever the determinant is.

@[simp]

theorem TauCeti.Probability.multivariateGaussianPDF_ne_top {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : multivariateGaussianPDF m S x ≠ ⊤

The ℝ≥0∞-valued density is finite at every covariance parameter.

theorem TauCeti.Probability.multivariateGaussianPDF_lt_top {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : multivariateGaussianPDF m S x < ⊤

The ℝ≥0∞-valued density is finite at every covariance parameter.

@[simp]

theorem TauCeti.Probability.toReal_multivariateGaussianPDF {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : (multivariateGaussianPDF m S x).toReal = multivariateGaussianPDFReal m S x

The ℝ≥0∞-valued density carries the real-valued one back through ENNReal.toReal.

theorem TauCeti.Probability.measurable_multivariateGaussianPDFReal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) : Measurable (multivariateGaussianPDFReal m S)

The real-valued density is measurable.

theorem TauCeti.Probability.measurable_multivariateGaussianPDF {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) : Measurable (multivariateGaussianPDF m S)

The ℝ≥0∞-valued density is measurable.

theorem TauCeti.Probability.stdGaussian_eq_withDensity {ι : Type u_1} [Fintype ι] : ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι) = MeasureTheory.volume.withDensity fun (x : EuclideanSpace ℝ ι) => ENNReal.ofReal ((2 * Real.pi) ^ (-↑(Fintype.card ι) / 2) * Real.exp (-‖x‖ ^ 2 / 2))

The standard Gaussian on EuclideanSpace ℝ ι has the isotropic Gaussian density.

theorem TauCeti.Probability.stdGaussian_eq_withDensity_norm (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ProbabilityTheory.stdGaussian E = MeasureTheory.volume.withDensity fun (x : E) => ENNReal.ofReal ((2 * Real.pi) ^ (-↑(Module.finrank ℝ E) / 2) * Real.exp (-‖x‖ ^ 2 / 2))

The standard Gaussian on a finite-dimensional real inner product space has the isotropic Gaussian density (2π)^(-d/2) * exp (-‖x‖² / 2), where d is the dimension.

@[simp]

theorem TauCeti.Probability.support_stdGaussian (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (ProbabilityTheory.stdGaussian E).support = Set.univ

The standard Gaussian measure on a finite-dimensional real inner product space has full support.

@[simp]

theorem TauCeti.Probability.support_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (m : EuclideanSpace ℝ ι) : (ProbabilityTheory.multivariateGaussian m S).support = ↑(AffineSubspace.mk' m (Matrix.toEuclideanLin S).range)

The support of a multivariate Gaussian measure with positive-semidefinite covariance is the affine range of its covariance.

theorem TauCeti.Probability.ae_mem_affineRange_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (m : EuclideanSpace ℝ ι) : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂ProbabilityTheory.multivariateGaussian m S, x ∈ ↑(AffineSubspace.mk' m (Matrix.toEuclideanLin S).range)

A multivariate Gaussian measure with positive-semidefinite covariance is almost surely in the affine range of its covariance.

theorem TauCeti.Probability.multivariateGaussian_eq_withDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hS : S.PosDef) (m : EuclideanSpace ℝ ι) : ProbabilityTheory.multivariateGaussian m S = MeasureTheory.volume.withDensity (multivariateGaussianPDF m S)

A nondegenerate multivariate Gaussian law is Lebesgue measure with the Gaussian density.

theorem TauCeti.Probability.hasPDF_of_hasLaw_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ ι} (hS : S.PosDef) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.multivariateGaussian m S) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A random vector with a nondegenerate multivariate Gaussian law has a density.

theorem TauCeti.Probability.pdf_eq_multivariateGaussianPDF_of_hasLaw_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ ι} (hS : S.PosDef) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.multivariateGaussian m S) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] multivariateGaussianPDF m S

The density of a nondegenerate multivariate Gaussian law is multivariateGaussianPDF.

theorem TauCeti.Probability.rnDeriv_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hS : S.PosDef) (m : EuclideanSpace ℝ ι) : (ProbabilityTheory.multivariateGaussian m S).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] multivariateGaussianPDF m S

The Radon–Nikodym derivative of a nondegenerate multivariate Gaussian law.

theorem TauCeti.Probability.mutuallySingular_multivariateGaussian_volume {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hS : ¬S.PosDef) (m : EuclideanSpace ℝ ι) : (ProbabilityTheory.multivariateGaussian m S).MutuallySingular MeasureTheory.volume

Every degenerate multivariate Gaussian law is singular. A positive-semidefinite but singular covariance carries the law on the proper affine subspace m + range (CFC.sqrt S); any other covariance makes the law a point mass.

theorem TauCeti.Probability.rnDeriv_multivariateGaussian_of_not_posDef {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (hS : ¬S.PosDef) (m : EuclideanSpace ℝ ι) : (ProbabilityTheory.multivariateGaussian m S).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] 0

A degenerate multivariate Gaussian law has vanishing Radon–Nikodym derivative.