Gaussian maximum likelihood

TheoremLog-density of the multivariate Gaussian#✓fully proved

Let \(J\) be a finite set with \(n\) elements, let \(\mu, x \in \mathbb{R}^J\), let \(S\) be a positive definite real \(J \times J\) matrix, and write \(\mathcal{N}(x \mid \mu, S)\) for the multivariate Gaussian density at \(x\) with mean \(\mu\) and covariance \(S\). Then \(\log \mathcal{N}(x \mid \mu, S) = -\frac{n}{2} \log (2\pi) - \frac{1}{2} \log \det S - \frac{1}{2} (x - \mu)^{\mathsf T} S^{-1} (x - \mu)\).

theorem log_multivariateGaussianPDFReal (μ : EuclideanSpace ℝ n) {S : Matrix n n ℝ}
    (hS : S.PosDef) (x : EuclideanSpace ℝ n) :
    log (multivariateGaussianPDFReal μ S x) = -(Fintype.card n / 2) * log (2 * π) -
      log S.det / 2 - ofLp (x - μ) ⬝ᵥ S⁻¹ *ᵥ ofLp (x - μ) / 2

Uses 1 · Used by 1

Statement usesMultivariate Gaussian density function

Used byThe weighted Gaussian log-likelihood via the scatter matrix

TheoremThe weighted Gaussian log-likelihood via the scatter matrix#✓fully proved

Let \(I\) be a finite set and \(J\) a finite set with \(n\) elements, let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with real weights \(w_i\) whose sum \(W = \sum_{i \in I} w_i\) is nonzero, let \(\mu \in \mathbb{R}^J\), let \(S\) be a positive definite real \(J \times J\) matrix, and let \(C(\mu)\) be the weighted scatter matrix of the \(x_i\) about \(\mu\). Write \(\mathcal{N}(x \mid \mu, S)\) for the multivariate Gaussian density at \(x\) with mean \(\mu\) and covariance \(S\). Then \(\sum_{i \in I} w_i \log \mathcal{N}(x_i \mid \mu, S) = -\frac{W}{2} \big(n \log (2\pi) + \log \det S + \operatorname{tr}(S^{-1} C(\mu))\big)\).

theorem sum_mul_log_multivariateGaussianPDFReal_eq {w : ι → ℝ} (hw : ∑ i, w i ≠ 0)
    (xs : ι → EuclideanSpace ℝ n) (μ : EuclideanSpace ℝ n) {S : Matrix n n ℝ} (hS : S.PosDef) :
    ∑ i, w i * log (multivariateGaussianPDFReal μ S (xs i)) =
      -((∑ i, w i) / 2) * (Fintype.card n * log (2 * π) + log S.det +
        (S⁻¹ * weightedScatter w xs μ).trace)

Uses 4 · Used by 3

Statement usesMultivariate Gaussian density function · Weighted scatter matrix

Proof usesLog-density of the multivariate Gaussian · Weighted quadratic forms as traces against the scatter matrix

Used byNo latent factors: the noise-variance MLE is the average sample variance · The weighted mean is the Gaussian MLE of the mean · The weighted Gaussian MLE when the sample covariance is positive definite

TheoremThe weighted mean is the Gaussian MLE of the mean#✓fully proved

Let \(I\) and \(J\) be finite sets, let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with real weights \(w_i\) such that \(\sum_i w_i > 0\), let \(m\) be their weighted mean, and let \(S\) be a positive definite real \(J \times J\) matrix. Write \(\mathcal{N}(x \mid \mu, S)\) for the multivariate Gaussian density at \(x\) with mean \(\mu\) and covariance \(S\). Then for every \(\mu \in \mathbb{R}^J\), \(\sum_{i \in I} w_i \log \mathcal{N}(x_i \mid \mu, S) \le \sum_{i \in I} w_i \log \mathcal{N}(x_i \mid m, S)\).

theorem sum_mul_log_multivariateGaussianPDFReal_le_weightedMean {w : ι → ℝ}
    (hw : 0 < ∑ i, w i) (xs : ι → EuclideanSpace ℝ n) (μ : EuclideanSpace ℝ n)
    {S : Matrix n n ℝ} (hS : S.PosDef) :
    ∑ i, w i * log (multivariateGaussianPDFReal μ S (xs i)) ≤
      ∑ i, w i * log (multivariateGaussianPDFReal (weightedMean w xs) S (xs i))

Uses 6 · Used by 1

Statement usesMultivariate Gaussian density function · Weighted mean

Proof usesThe weighted Gaussian log-likelihood via the scatter matrix · Weighted quadratic forms as traces against the scatter matrix · The bias-variance split of a weighted quadratic form · Weighted scatter matrix

Used byThe mean MLE is the sample mean

TheoremThe weighted Gaussian MLE when the sample covariance is positive definite#✓fully proved

Let \(I\) and \(J\) be finite sets, let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with real weights \(w_i\) such that \(\sum_i w_i > 0\), let \(m\) be their weighted mean, and let \(C\) be their weighted scatter matrix about \(m\) (the weighted sample covariance); assume \(C\) is positive definite. Write \(\mathcal{N}(x \mid \mu, S)\) for the multivariate Gaussian density at \(x\) with mean \(\mu\) and covariance \(S\). Then for every \(\mu \in \mathbb{R}^J\) and every positive definite real \(J \times J\) matrix \(S\), \(\sum_{i \in I} w_i \log \mathcal{N}(x_i \mid \mu, S) \le \sum_{i \in I} w_i \log \mathcal{N}(x_i \mid m, C)\).

theorem sum_mul_log_multivariateGaussianPDFReal_le_of_posDef {w : ι → ℝ} (hW : 0 < ∑ i, w i)
    {xs : ι → EuclideanSpace ℝ n} (hC : (weightedScatter w xs (weightedMean w xs)).PosDef)
    (μ : EuclideanSpace ℝ n) {S : Matrix n n ℝ} (hS : S.PosDef) :
    ∑ i, w i * log (multivariateGaussianPDFReal μ S (xs i)) ≤
      ∑ i, w i * log (multivariateGaussianPDFReal (weightedMean w xs)
        (weightedScatter w xs (weightedMean w xs)) (xs i))

Uses 7 · Used by 2

Statement usesMultivariate Gaussian density function · Weighted mean · Weighted scatter matrix

Proof usesLog-determinant trace inequality · The weighted Gaussian log-likelihood via the scatter matrix · Weighted quadratic forms as traces against the scatter matrix · The bias-variance split of a weighted quadratic form

Used byThe probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · The weighted Gaussian MLE for points in general position

TheoremThe weighted Gaussian MLE for points in general position#✓fully proved

Let \(I\) be a nonempty finite set and \(J\) a finite set, and let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with positive weights \(w_i > 0\) that do not all lie in an affine hyperplane: for every nonzero \(v \in \mathbb{R}^J\) there are \(i, j \in I\) with \(\langle v, x_i \rangle \ne \langle v, x_j \rangle\). Let \(m\) be their weighted mean and \(C\) their weighted scatter matrix about \(m\) (the weighted sample covariance), and write \(\mathcal{N}(x \mid \mu, S)\) for the multivariate Gaussian density at \(x\) with mean \(\mu\) and covariance \(S\). Then for every \(\mu \in \mathbb{R}^J\) and every positive definite real \(J \times J\) matrix \(S\), \(\sum_{i \in I} w_i \log \mathcal{N}(x_i \mid \mu, S) \le \sum_{i \in I} w_i \log \mathcal{N}(x_i \mid m, C)\).

theorem sum_mul_log_multivariateGaussianPDFReal_le {w : ι → ℝ} (hw : ∀ i, 0 < w i)
    {xs : ι → EuclideanSpace ℝ n}
    (hspan : ∀ v : EuclideanSpace ℝ n, v ≠ 0 → ∃ i j, ⟪v, xs i⟫ ≠ ⟪v, xs j⟫) [Nonempty ι]
    (μ : EuclideanSpace ℝ n) {S : Matrix n n ℝ} (hS : S.PosDef) :
    ∑ i, w i * log (multivariateGaussianPDFReal μ S (xs i)) ≤
      ∑ i, w i * log (multivariateGaussianPDFReal (weightedMean w xs)
        (weightedScatter w xs (weightedMean w xs)) (xs i))

Uses 5 · Used by 1

Statement usesMultivariate Gaussian density function · Weighted mean · Weighted scatter matrix

Proof usesThe weighted Gaussian MLE when the sample covariance is positive definite · Weighted scatter matrices of points in general position are positive definite

Used byThe mean and covariance updates maximize each component term

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.