Theorems · Definition · probability

ProbabilityTheory.multivariateGaussian

{ι : Type u_1} →
  [Fintype ι] → [DecidableEq ι] → EuclideanSpace ℝ ι → 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).

Defined in

Mathlib.Probability.Distributions.Gaussian.Multivariate

Cited by

19 results in Mathlib

Foundations

Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEq