Multivariate normal distribution

DefinitionStandard Gaussian density function#✓fully proved

Let \(\iota\) be a finite set of size \(n\). The standard Gaussian density on the Euclidean space \(\mathbb{R}^\iota\) is the real-valued function \(v \mapsto (2\pi)^{-n/2} \exp(-\|v\|^2/2)\).

noncomputable def stdGaussianPDFReal (v : EuclideanSpace ℝ ι) : ℝ :=
  ((√(2 * Real.pi)) ^ Fintype.card ι)⁻¹ * Real.exp (-(‖v‖ ^ 2) / 2)

Used by 3

Used byThe multivariate Gaussian density · Standard Gaussian measure via its density · The standard Gaussian has a density

DefinitionStandard Gaussian measure via its density#✓fully proved

Let \(\iota\) be a finite set of size \(n\). This is the measure on the Euclidean space \(\mathbb{R}^\iota\) with density \(v \mapsto (2\pi)^{-n/2} \exp(-\|v\|^2/2)\) with respect to Lebesgue measure.

noncomputable def stdGaussianDensityMeasure : Measure (EuclideanSpace ℝ ι) :=
  volume.withDensity fun v => ENNReal.ofReal (stdGaussianPDFReal v)

Uses 1 · Used by 1

Statement usesStandard Gaussian density function

Used byThe standard Gaussian has a density

TheoremThe standard Gaussian has a density#✓fully proved

Let \(\iota\) be a finite set of size \(n\). The standard Gaussian measure on the Euclidean space \(\mathbb{R}^\iota\) has density \(v \mapsto (2\pi)^{-n/2} \exp(-\|v\|^2/2)\) with respect to Lebesgue measure.

theorem stdGaussian_eq_withDensity :
    stdGaussian (EuclideanSpace ℝ ι) =
      volume.withDensity fun v => ENNReal.ofReal (stdGaussianPDFReal v)

Uses 2 · Used by 1

Statement usesStandard Gaussian density function

Proof usesStandard Gaussian measure via its density

Used byThe multivariate Gaussian density

TheoremPushforward of a measure with density#✓fully proved

Let \(e : \alpha \to \beta\) be a measurable equivalence between measurable spaces, \(\nu\) a measure on \(\alpha\) and \(g : \alpha \to [0, \infty]\) any function. Then the pushforward under \(e\) of the measure with density \(g\) with respect to \(\nu\) is the measure with density \(g \circ e^{-1}\) with respect to the pushforward \(e_*\nu\) of \(\nu\).

theorem map_withDensity_measurableEquiv {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (e : α ≃ᵐ β) (ν : Measure α) {g : α → ENNReal} :
    (ν.withDensity g).map e = (ν.map e).withDensity (g ∘ e.symm)

Used by 1

Used byThe multivariate Gaussian density

DefinitionThe affine change of variables as a measurable equivalence#✓fully proved

Let \(\iota\) be a finite type, \(\mu \in \mathbb{R}^\iota\) and \(A\) a real \(\iota \times \iota\) matrix with nonzero determinant. The map \(x \mapsto \mu + Ax\) is a measurable equivalence of the Euclidean space \(\mathbb{R}^\iota\) with itself, with inverse \(y \mapsto A^{-1}(y - \mu)\).

MetaMathlibExt.affineEquiv · 20 lines

noncomputable def affineEquiv (μ : EuclideanSpace ℝ ι) (A : Matrix ι ι ℝ) (hA : IsUnit A.det) :
    EuclideanSpace ℝ ι ≃ᵐ EuclideanSpace ℝ ι where
  toFun x := μ + toEuclideanCLM (𝕜 := ℝ) A x
  invFun y := toEuclideanCLM (𝕜 := ℝ) A⁻¹ (y - μ)
  left_inv x := by
    simp only [add_sub_cancel_left]
    rw [← ContinuousLinearMap.comp_apply, ← ContinuousLinearMap.mul_def, ← map_mul,
      nonsing_inv_mul _ hA, map_one]
    rfl
  right_inv y := by
    simp only
    rw [← ContinuousLinearMap.comp_apply, ← ContinuousLinearMap.mul_def, ← map_mul,
      mul_nonsing_inv _ hA, map_one]
    exact add_sub_cancel μ y
  measurable_toFun := by
    change Measurable fun x => μ + toEuclideanCLM (𝕜 := ℝ) A x
    fun_prop
  measurable_invFun := by
    change Measurable fun y => toEuclideanCLM (𝕜 := ℝ) A⁻¹ (y - μ)
    fun_prop

Used by 3

Used byLande's gradient of mean fitness for multivariate traits · Lebesgue measure under an invertible affine map · The multivariate Gaussian density

TheoremLebesgue measure under an invertible affine map#✓fully proved

Let \(\iota\) be a finite type, \(\mu \in \mathbb{R}^\iota\) and \(A\) a real \(\iota \times \iota\) matrix with nonzero determinant. The pushforward of Lebesgue measure on the Euclidean space \(\mathbb{R}^\iota\) under the measurable equivalence \(x \mapsto \mu + Ax\) equals \(|\det A|^{-1}\) times Lebesgue measure.

theorem map_affineEquiv_volume (μ : EuclideanSpace ℝ ι) (A : Matrix ι ι ℝ) (hA : IsUnit A.det) :
    (volume : Measure (EuclideanSpace ℝ ι)).map (affineEquiv μ A hA) =
      ENNReal.ofReal |(A.det)⁻¹| • volume

Uses 1 · Used by 2

Statement usesThe affine change of variables as a measurable equivalence

Used byLande's gradient of mean fitness for multivariate traits · The multivariate Gaussian density

DefinitionMultivariate Gaussian density function#✓fully proved

Let \(\iota\) be a finite set of size \(n\). For \(\mu, x \in \mathbb{R}^\iota\) and a real \(\iota \times \iota\) matrix \(S\), this is the real number

\[\frac{1}{(2\pi)^{n/2}\sqrt{\det S}} \exp\left(-\frac{(x - \mu)^\top S^{-1}(x - \mu)}{2}\right).\]

It is defined for every \(S\), with the conventions \(\sqrt{t} = 0\) for \(t < 0\), \(1/0 = 0\) and \(S^{-1} = 0\) for singular \(S\), so its value is \(0\) when \(\det S \le 0\).

noncomputable def multivariateGaussianPDFReal (μ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ)
    (x : EuclideanSpace ℝ ι) : ℝ :=
  ((√(2 * Real.pi)) ^ Fintype.card ι)⁻¹ * (√S.det)⁻¹ *
    Real.exp (-(ofLp (x - μ) ⬝ᵥ S⁻¹ *ᵥ ofLp (x - μ)) / 2)

Used by 27

Used byLande's gradient of mean fitness for multivariate traits · The marginal law of the phenotype given the causal variant · The regression Bayes factor is the Wakefield ABF · Single-effect likelihood-ratio identity · Posterior inclusion probabilities of the single-effect regression · Component term of the EM objective for full-covariance Gaussian mixtures · The mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood · The covariance update is positive definite · The weight update maximizes the weights term of the full-covariance mixture · Probabilistic PCA MLE when the sample covariance has the model form · Probabilistic PCA log-likelihood · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · The mean MLE is the sample mean · The log-likelihood of no data is zero · No latent factors: the noise-variance MLE is the average sample variance · The density of the probabilistic PCA observation · The multivariate Gaussian density · Log-density of the multivariate Gaussian · The weighted Gaussian log-likelihood via the scatter matrix · The weighted mean is the Gaussian MLE of the mean · The weighted Gaussian MLE when the sample covariance is positive definite · The weighted Gaussian MLE for points in general position

TheoremQuadratic form of the inverse square root#✓fully proved

Let \(\iota\) be a finite type, \(S\) a positive definite real \(\iota \times \iota\) matrix and \(S^{1/2}\) its positive semidefinite square root. Then for every \(u\) in the Euclidean space \(\mathbb{R}^\iota\), \(\|(S^{1/2})^{-1} u\|^2 = u^\top S^{-1} u\).

theorem norm_sq_sqrt_inv_apply {S : Matrix ι ι ℝ} (hS : S.PosDef) (u : EuclideanSpace ℝ ι) :
    ‖toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S)⁻¹ u‖ ^ 2 = ofLp u ⬝ᵥ S⁻¹ *ᵥ ofLp u

Used by 2

Used byLande's gradient of mean fitness for multivariate traits · The multivariate Gaussian density

TheoremThe multivariate Gaussian density#✓fully proved

Let \(\iota\) be a finite set of size \(n\), let \(\mu \in \mathbb{R}^\iota\) and let \(S\) be a positive definite real \(\iota \times \iota\) matrix. Then the multivariate Gaussian measure on the Euclidean space \(\mathbb{R}^\iota\) with mean \(\mu\) and covariance matrix \(S\) (the image of the standard Gaussian under \(x \mapsto \mu + S^{1/2} x\)) has density

\[\frac{1}{(2\pi)^{n/2} \sqrt{\det S}} \exp\left(-\frac{(x - \mu)^\top S^{-1} (x - \mu)}{2}\right)\]

with respect to Lebesgue measure.

theorem multivariateGaussian_eq_withDensity (μ : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ}
    (hS : S.PosDef) :
    multivariateGaussian μ S =
      volume.withDensity fun x => ENNReal.ofReal (multivariateGaussianPDFReal μ S x)

Uses 7 · Used by 3

Statement usesMultivariate Gaussian density function

Proof usesThe affine change of variables as a measurable equivalence · Lebesgue measure under an invertible affine map · Pushforward of a measure with density · Quadratic form of the inverse square root · Standard Gaussian density function · The standard Gaussian has a density

Used byLande's gradient of mean fitness for multivariate traits · The marginal law of the phenotype given the causal variant · The density of the probabilistic PCA observation

TheoremSheppard's formula (Gaussian arcsine law)#●ready to prove

Let \(\rho\) be a real number with \(-1 < \rho < 1\), and let \(\gamma\) be the multivariate Gaussian measure on \(\mathbb{R}^2\) with mean \(0\) and covariance matrix whose diagonal entries are \(1\) and whose off-diagonal entries are \(\rho\) (the law of a standard bivariate normal vector with correlation \(\rho\)). Then the open first quadrant \(\{x \in \mathbb{R}^2 : x_1 > 0,\ x_2 > 0\}\) has \(\gamma\)-probability \(\frac{1}{4} + \frac{\arcsin \rho}{2\pi}\).

public theorem_wanted sheppard_quadrant_probability_arcsine (ρ : ℝ) (hρ : ρ ∈ Set.Ioo (-1) 1) :
    let S : Matrix (Fin 2) (Fin 2) ℝ := Matrix.of (fun i j => if i = j then 1 else ρ);
    (ProbabilityTheory.multivariateGaussian 0 S).real {x | 0 < x 0 ∧ 0 < x 1}
      = 1 / 4 + Real.arcsin ρ / (2 * Real.pi)

Sources

• Y. L. Tong, The Multivariate Normal Distribution, Springer, 1990, Ch. 3; W. F. Sheppard, "On the application of the theory of error to cases of normal distribution and normal correlation", Phil. Trans. R. Soc. Lond. A 192 (1899), 101–167; https://en.wikipedia.org/wiki/Multivariate_normal_distribution

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.