Theorems · Theorem · probability

ProbabilityTheory.covariance_eval_multivariateGaussian

∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {μ : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ},
  S.PosSemidef →
    ∀ (i j : ι),
      ProbabilityTheory.covariance (fun x => x.ofLp i) (fun x => x.ofLp j)
          (ProbabilityTheory.multivariateGaussian μ S) =
        S i j

Defined in

Mathlib.Probability.Distributions.Gaussian.Multivariate

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq