Theorems · Theorem · probability

ProbabilityTheory.measurePreserving_eval_multivariateGaussian

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

Defined in: Mathlib.Probability.Distributions.Gaussian.Multivariate
Cited by: 0 results in Mathlib
Foundations: Depth 320 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.

Cites26

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

DFunLike.coeproof · cited by 62,936
Realstatement and proof · cited by 25,697
MeasureTheory.Measureproof · cited by 10,939
ENNRealstatement · cited by 9,879
Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
MeasureTheory.Measure.mapproof · cited by 858
WithLp.ofLpstatement and proof · cited by 323
EuclideanSpacestatement and proof · cited by 307
Real.toNNRealstatement and proof · cited by 267
MeasureTheory.MeasurePreservingstatement · cited by 259
ProbabilityTheory.varianceproof · cited by 104

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.