Theorems · Theorem · probability

ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis

∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E]
  [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [BorelSpace E] (b : OrthonormalBasis ι ℝ E),
  ProbabilityTheory.stdGaussian E =
    MeasureTheory.Measure.map (fun x => ∑ i, x i • b i)
      (MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1)

The definition of stdGaussian does not depend on the basis.

Defined in

Mathlib.Probability.Distributions.Gaussian.Multivariate

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpace