Multivariate Gaussian distributions

theorem ProbabilityTheory.covMatrix_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : covMatrix (stdGaussian E) = 1

theorem ProbabilityTheory.inner_toEuclideanCLM {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Matrix ι ι ℝ} (x y : EuclideanSpace ℝ ι) : inner ℝ x ((Matrix.toEuclideanCLM S) y) = ⇑((EuclideanSpace.basisFun ι ℝ).toBasis.repr x) ⬝ᵥ S.mulVec ⇑((EuclideanSpace.basisFun ι ℝ).toBasis.repr y)

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