Weighted means and scatter matrices

DefinitionWeighted mean#✓fully proved

Let \(I\) be a finite set and \(J\) an index set, and let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with real weights \(w_i\). Their weighted mean is the point \(\big(\sum_{i \in I} w_i\big)^{-1} \sum_{i \in I} w_i x_i\) of \(\mathbb{R}^J\), that is \(\sum_i w_i x_i / \sum_i w_i\), with the convention \(0^{-1} = 0\) when the weights sum to \(0\).

noncomputable def weightedMean (w : ι → ℝ) (xs : ι → EuclideanSpace ℝ n) : EuclideanSpace ℝ n :=
  (∑ i, w i)⁻¹ • ∑ i, w i • xs i

Used by 9

Used byMean update of the full-covariance Gaussian mixture · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · The mean MLE is the sample mean · Sample mean · 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 · The bias-variance split of a weighted quadratic form · Weighted residuals sum to zero

DefinitionWeighted scatter matrix#✓fully proved

Let \(I\) be a finite set and \(J\) an index set, let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with real weights \(w_i\), and let \(\mu \in \mathbb{R}^J\). The weighted scatter matrix of the \(x_i\) about \(\mu\) is the real \(J \times J\) matrix

\[ C = \Big(\sum_{i \in I} w_i\Big)^{-1} \sum_{i \in I} w_i \, (x_i - \mu)(x_i - \mu)^{\mathsf T}, \]

with the convention \(0^{-1} = 0\) when the weights sum to \(0\). When \(\mu\) is the weighted mean of the \(x_i\), it is the weighted sample covariance.

noncomputable def weightedScatter (w : ι → ℝ) (xs : ι → EuclideanSpace ℝ n)
    (μ : EuclideanSpace ℝ n) : Matrix n n ℝ :=
  (∑ i, w i)⁻¹ • ∑ i, w i • vecMulVec (ofLp (xs i - μ)) (ofLp (xs i - μ))

Used by 11

Used byCovariance update of the full-covariance Gaussian mixture · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · No latent factors: the noise-variance MLE is the average sample variance · Sample covariance · 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 · Quadratic form of a weighted scatter matrix · Weighted quadratic forms as traces against the scatter matrix · Weighted scatter matrices of points in general position are positive definite

TheoremWeighted residuals sum to zero#✓fully proved

Let \(I\) be a finite set and \(J\) any index set, let \(x_i \in \mathbb{R}^J\) (\(i \in I\)) be points with real weights \(w_i\) such that \(\sum_i w_i \ne 0\), and let \(m\) be their weighted mean. Then \(\sum_{i \in I} w_i (x_i - m) = 0\).

theorem sum_smul_sub_weightedMean {w : ι → ℝ} (hw : ∑ i, w i ≠ 0)
    (xs : ι → EuclideanSpace ℝ n) : ∑ i, w i • (xs i - weightedMean w xs) = 0

Uses 1 · Used by 1

Statement usesWeighted mean

Used byThe bias-variance split of a weighted quadratic form

TheoremThe bias-variance split of a weighted quadratic form#✓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 \ne 0\), let \(m\) be their weighted mean, let \(A\) be a symmetric real \(J \times J\) matrix, and let \(\mu \in \mathbb{R}^J\). Then

\[ \sum_{i \in I} w_i \, (x_i - \mu)^{\mathsf T} A \, (x_i - \mu) = \sum_{i \in I} w_i \, (x_i - m)^{\mathsf T} A \, (x_i - m) + \Big(\sum_{i \in I} w_i\Big) (m - \mu)^{\mathsf T} A \, (m - \mu). \]

theorem sum_mul_quad_sub_eq {w : ι → ℝ} (hw : ∑ i, w i ≠ 0) (xs : ι → EuclideanSpace ℝ n)
    {A : Matrix n n ℝ} (hA : Aᵀ = A) (μ : EuclideanSpace ℝ n) :
    ∑ i, w i * (ofLp (xs i - μ) ⬝ᵥ A *ᵥ ofLp (xs i - μ)) =
      ∑ i, w i * (ofLp (xs i - weightedMean w xs) ⬝ᵥ A *ᵥ ofLp (xs i - weightedMean w xs)) +
        (∑ i, w i) * (ofLp (weightedMean w xs - μ) ⬝ᵥ A *ᵥ ofLp (weightedMean w xs - μ))

Uses 2 · Used by 2

Statement usesWeighted mean

Proof usesWeighted residuals sum to zero

Used byThe weighted mean is the Gaussian MLE of the mean · The weighted Gaussian MLE when the sample covariance is positive definite

TheoremWeighted quadratic forms as traces against the scatter matrix#✓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 \ne 0\), let \(A\) be a real \(J \times J\) matrix, let \(\mu \in \mathbb{R}^J\), and let \(C\) be the weighted scatter matrix of the \(x_i\) about \(\mu\). Then

\[ \sum_{i \in I} w_i \, (x_i - \mu)^{\mathsf T} A \, (x_i - \mu) = \Big(\sum_{i \in I} w_i\Big) \operatorname{tr}(A C). \]

theorem sum_mul_quad_eq_trace {w : ι → ℝ} (hw : ∑ i, w i ≠ 0) (xs : ι → EuclideanSpace ℝ n)
    (A : Matrix n n ℝ) (μ : EuclideanSpace ℝ n) :
    ∑ i, w i * (ofLp (xs i - μ) ⬝ᵥ A *ᵥ ofLp (xs i - μ)) =
      (∑ i, w i) * (A * weightedScatter w xs μ).trace

Uses 1 · Used by 3

Statement usesWeighted scatter matrix

Used byThe 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

TheoremQuadratic form of a weighted scatter matrix#✓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\), let \(\mu \in \mathbb{R}^J\), and let \(C\) be the weighted scatter matrix of the \(x_i\) about \(\mu\). Then for every \(u \in \mathbb{R}^J\),

\[ u^{\mathsf T} C u = \Big(\sum_{i \in I} w_i\Big)^{-1} \sum_{i \in I} w_i \big(u \cdot (x_i - \mu)\big)^2, \]

with the convention \(0^{-1} = 0\).

theorem dotProduct_weightedScatter_mulVec (w : ι → ℝ) (xs : ι → EuclideanSpace ℝ n)
    (μ : EuclideanSpace ℝ n) (u : n → ℝ) :
    u ⬝ᵥ weightedScatter w xs μ *ᵥ u =
      (∑ i, w i)⁻¹ * ∑ i, w i * (u ⬝ᵥ ofLp (xs i - μ)) ^ 2

Uses 1 · Used by 1

Statement usesWeighted scatter matrix

Used byWeighted scatter matrices of points in general position are positive definite

TheoremWeighted scatter matrices of points in general position are positive definite#✓fully proved

Let \(I\) and \(J\) be finite sets 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\). Then for every \(\mu \in \mathbb{R}^J\) the weighted scatter matrix of the \(x_i\) about \(\mu\) is positive definite.

theorem weightedScatter_posDef {w : ι → ℝ} (hw : ∀ i, 0 < w i) {xs : ι → EuclideanSpace ℝ n}
    (hspan : ∀ v : EuclideanSpace ℝ n, v ≠ 0 → ∃ i j, ⟪v, xs i⟫ ≠ ⟪v, xs j⟫)
    (μ : EuclideanSpace ℝ n) : (weightedScatter w xs μ).PosDef

Uses 2 · Used by 2

Statement usesWeighted scatter matrix

Proof usesQuadratic form of a weighted scatter matrix

Used byThe covariance update is positive definite · The weighted Gaussian MLE for points in general position

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.