Theorems · Theorem · probability

ProbabilityTheory.charFun_multivariateGaussian

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

Defined in: Mathlib.Probability.Distributions.Gaussian.Multivariate
Cited by: 0 results in Mathlib
Foundations: Depth 318 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
ENNRealstatement · cited by 9,879
Fintypestatement and proof · cited by 7,736
Complexstatement · cited by 5,565
Matrixstatement and proof · cited by 4,303
Complex.ofRealstatement and proof · cited by 1,654
Inner.innerstatement and proof · cited by 1,089
Complex.Istatement and proof · cited by 866
Complex.expstatement and proof · cited by 612
WithLp.ofLpstatement and proof · cited by 323
EuclideanSpacestatement and proof · cited by 307
Matrix.mulVecstatement and proof · cited by 267

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.