k-means clustering

DefinitionCentroid#✓fully proved

Let \(x_i\) be points in a real inner product space and \(s\) a finite set of indices. The centroid of the points indexed by \(s\) is \(\frac{1}{|s|} \sum_{i \in s} x_i\); when \(s\) is empty it is the zero vector.

noncomputable def centroid (x : ι → E) (s : Finset ι) : E :=
  (s.card : ℝ)⁻¹ • ∑ i ∈ s, x i

Used by 3

Used byThe centroid update step · The update step never increases the cost · Sum of squared distances about the centroid

TheoremSum of squared distances about the centroid#✓fully proved

Let \(x_i\) (\(i \in \iota\)) be points in a real inner product space \(E\), let \(s\) be a finite set of indices, and let \(\mu\) be the centroid of the points \(x_i\) with \(i \in s\). Then for every point \(c \in E\),

\[ \sum_{i \in s} \|x_i - c\|^2 = \sum_{i \in s} \|x_i - \mu\|^2 + |s| \, \|\mu - c\|^2. \]

Consequently the centroid minimizes the sum of squared distances to the points \(x_i\), \(i \in s\).

theorem sum_sq_eq (x : ι → E) (s : Finset ι) (c : E) :
    ∑ i ∈ s, ‖x i - c‖ ^ 2 =
      ∑ i ∈ s, ‖x i - centroid x s‖ ^ 2 + s.card * ‖centroid x s - c‖ ^ 2

Uses 1 · Used by 1

Statement usesCentroid

Used byThe update step never increases the cost

DefinitionNearest-center assignment#✓fully proved

Given points \(x_i\) (\(i \in \iota\)) in a normed additive commutative group \(E\) and centers \(c_0, \dots, c_{k-1} \in E\), an assignment \(a : \iota \to \{0, \dots, k-1\}\) assigns every point to a nearest center when \(\|x_i - c_{a(i)}\| \le \|x_i - c_j\|\) for every index \(i \in \iota\) and every \(j < k\).

def Nearest (x : ι → E) (c : Fin k → E) (a : ι → Fin k) : Prop :=
  ∀ i j, ‖x i - c (a i)‖ ≤ ‖x i - c j‖

Used by 7

Used byThe cost never increases along a run of Lloyd's algorithm · One round of Lloyd's algorithm never increases the cost · The assignment step never increases the cost · Nearest-center assignments exist · Runs of Lloyd's algorithm exist · Run of Lloyd's algorithm · The k-means assignment step is the zero-variance limit of the E-step

TheoremNearest-center assignments exist#✓fully proved

For any points \(x_i\) in a normed additive commutative group and any centers \(c_0, \dots, c_{k-1}\) with \(k \ge 1\), there is an assignment that sends every point to a nearest center.

theorem exists_nearest (x : ι → E) (c : Fin k → E) (hk : 0 < k) : ∃ a, Nearest x c a

Uses 1 · Used by 1

Statement usesNearest-center assignment

Used byRuns of Lloyd's algorithm exist

DefinitionThe k-means cost#✓fully proved

For points \(x_i\) (\(i \in \iota\), a finite type) in a normed additive commutative group, an assignment \(a\) of each point \(i\) to a cluster \(a(i) \in \{0, \dots, k-1\}\) and centers \(c_0, \dots, c_{k-1}\), the \(k\)-means cost is \(\sum_{i \in \iota} \lVert x_i - c_{a(i)} \rVert^2\), the sum of the squared distances from the points to their assigned centers.

def cost (x : ι → E) (a : ι → Fin k) (c : Fin k → E) : ℝ := ∑ i, ‖x i - c (a i)‖ ^ 2

Used by 5

Used byThe cost never increases along a run of Lloyd's algorithm · The update step never increases the cost · The cost as a sum over clusters · One round of Lloyd's algorithm never increases the cost · The assignment step never increases the cost

TheoremThe cost as a sum over clusters#✓fully proved

For points \(x_i\) (\(i \in \iota\), a finite type) in a normed additive commutative group, an assignment \(a\) of each point \(i\) to a cluster \(a(i) \in \{0, \dots, k-1\}\) and centers \(c_0, \dots, c_{k-1}\), the \(k\)-means cost equals \(\sum_{j} \sum_{i : a(i) = j} \lVert x_i - c_j \rVert^2\): for each cluster \(j\), add up the squared distances from the points assigned to \(j\) to its center \(c_j\).

theorem cost_eq_sum_clusters (x : ι → E) (a : ι → Fin k) (c : Fin k → E) :
    cost x a c = ∑ j, ∑ i ∈ univ.filter (fun i => a i = j), ‖x i - c j‖ ^ 2

Uses 1 · Used by 1

Statement usesThe k-means cost

Used byThe update step never increases the cost

DefinitionThe centroid update step#✓fully proved

Let \(x_i\) (\(i \in \iota\), a finite type) be points in a real inner product space and let \(a\) assign each point \(i\) to a cluster \(a(i) \in \{0, \dots, k-1\}\). The updated centers send each cluster \(j\) to the centroid of the points \(x_i\) with \(a(i) = j\). A cluster with no points gets the center \(0\), which does not affect the \(k\)-means cost of \(a\).

noncomputable def centers (x : ι → E) (a : ι → Fin k) : Fin k → E :=
  fun j => centroid x (univ.filter fun i => a i = j)

Uses 1 · Used by 6

Statement usesCentroid

Used byThe cost never increases along a run of Lloyd's algorithm · The update step never increases the cost · One round of Lloyd's algorithm never increases the cost · Runs of Lloyd's algorithm exist · Run of Lloyd's algorithm · The M-step in the zero-variance limit

TheoremThe update step never increases the cost#✓fully proved

For a fixed assignment, the centroids are the best centers.

theorem cost_centers_le (x : ι → E) (a : ι → Fin k) (c : Fin k → E) :
    cost x a (centers x a) ≤ cost x a c

Uses 5 · Used by 1

Statement usesThe centroid update step · The k-means cost

Proof usesCentroid · The cost as a sum over clusters · Sum of squared distances about the centroid

Used byOne round of Lloyd's algorithm never increases the cost

TheoremThe assignment step never increases the cost#✓fully proved

For fixed centers, nearest-center assignment is optimal.

theorem cost_nearest_le {x : ι → E} {c : Fin k → E} {a' : ι → Fin k}
    (h : Nearest x c a') (a : ι → Fin k) : cost x a' c ≤ cost x a c

Uses 2 · Used by 1

Statement usesNearest-center assignment · The k-means cost

Used byOne round of Lloyd's algorithm never increases the cost

TheoremOne round of Lloyd's algorithm never increases the cost#✓fully proved

Recompute the centers, then reassign every point to a nearest new center.

theorem cost_lloyd_le {x : ι → E} {a a' : ι → Fin k} (c : Fin k → E)
    (h : Nearest x (centers x a) a') : cost x a' (centers x a) ≤ cost x a c

Uses 5 · Used by 1

Statement usesNearest-center assignment · The centroid update step · The k-means cost

Proof usesThe update step never increases the cost · The assignment step never increases the cost

Used byThe cost never increases along a run of Lloyd's algorithm

DefinitionRun of Lloyd's algorithm#✓fully proved

Let \(x_i\) (\(i \in \iota\), a finite index set) be points in a real inner product space \(E\). Sequences of assignments \(a_t : \iota \to \{0, \dots, k-1\}\) and of centers \(c_t : \{0, \dots, k-1\} \to E\), indexed by \(t \in \mathbb{N}\), form a run of Lloyd's algorithm when for every \(t\): for each \(j < k\) the center \(c_{t+1}(j)\) is the centroid of the cluster \(\{i : a_t(i) = j\}\) (the zero vector if this cluster is empty), and \(a_{t+1}\) assigns every point to a nearest center of \(c_{t+1}\). The initial assignment \(a_0\) and centers \(c_0\) are arbitrary.

def IsRun (x : ι → E) (as : ℕ → ι → Fin k) (cs : ℕ → Fin k → E) : Prop :=
  ∀ t, cs (t + 1) = centers x (as t) ∧ Nearest x (cs (t + 1)) (as (t + 1))

Uses 2 · Used by 2

Statement usesNearest-center assignment · The centroid update step

Used byThe cost never increases along a run of Lloyd's algorithm · Runs of Lloyd's algorithm exist

TheoremThe cost never increases along a run of Lloyd's algorithm#✓fully proved

The cost never increases along a run of Lloyd's algorithm.

theorem IsRun.antitone {x : ι → E} {as : ℕ → ι → Fin k} {cs : ℕ → Fin k → E}
    (h : IsRun x as cs) : Antitone fun t => cost x (as t) (cs t)

Uses 5

Statement usesRun of Lloyd's algorithm · The k-means cost

Proof usesNearest-center assignment · The centroid update step · One round of Lloyd's algorithm never increases the cost

TheoremRuns of Lloyd's algorithm exist#✓fully proved

Let \(x_i\) (\(i \in \iota\), a finite type) be points in a real inner product space and let \(k \ge 1\). Every starting assignment \(a_0\) of the points to clusters \(0, \dots, k-1\) and every choice of starting centers \(c_0\) extend to a run of Lloyd's algorithm: there are assignments \(a_t\) and centers \(c_t\) for \(t \in \mathbb{N}\), equal to \(a_0\) and \(c_0\) at \(t = 0\), that form a run.

theorem exists_run (x : ι → E) (hk : 0 < k) (a₀ : ι → Fin k) (c₀ : Fin k → E) :
    ∃ as cs, as 0 = a₀ ∧ cs 0 = c₀ ∧ IsRun x as cs

Uses 4

Statement usesRun of Lloyd's algorithm

Proof usesNearest-center assignment · The centroid update step · Nearest-center assignments exist

DefinitionResponsibilities with a common variance#✓fully proved

Given weights \(w_1, \dots, w_K \in \mathbb{R}\), means \(\mu_1, \dots, \mu_K \in \mathbb{R}^d\) and a real \(v\), the common-variance responsibility of component \(k\) at a point \(x \in \mathbb{R}^d\) is

\[ r_v(x, k) = \frac{w_k \, \mathcal{N}(x \mid \mu_k, vI)} {\sum_i w_i \, \mathcal{N}(x \mid \mu_i, vI)}, \]

where, for \(v > 0\), \(\mathcal{N}(x \mid \mu, vI)\) is the isotropic Gaussian density with mean \(\mu\) and covariance \(vI\), and for \(v \le 0\) it is \(1\) if \(d = 0\) and \(0\) if \(d \ge 1\). A quotient with denominator \(0\) is \(0\).

noncomputable def softAssign (w : Fin K → ℝ) (μ : Fin K → EuclideanSpace ℝ (Fin d)) (v : ℝ)
    (x : EuclideanSpace ℝ (Fin d)) (k : Fin K) : ℝ :=
  w k * isoGaussPDF (μ k) v.toNNReal x / ∑ i, w i * isoGaussPDF (μ i) v.toNNReal x

Uses 1 · Used by 7

Statement usesIsotropic Gaussian density

Used byThe k-means assignment step is the zero-variance limit of the E-step · The Gaussian-mixture M-step mean is the common-variance M-step mean · The Gaussian-mixture responsibilities are the common-variance responsibilities · Common-variance responsibilities relative to a fixed component · Common-variance M-step mean · Responsibilities in the zero-variance limit · The M-step in the zero-variance limit

TheoremThe Gaussian-mixture responsibilities are the common-variance responsibilities#✓fully proved

Let \(\theta\) be valid parameters of an isotropic Gaussian mixture with \(K\) components on \(\mathbb{R}^d\), with weights \(w_k\), means \(\mu_k\) and variances all equal to a real number \(v\). Then for every point \(x \in \mathbb{R}^d\) and every component \(k\), the responsibility of \(k\) at \(x\) under \(\theta\) equals the common-variance responsibility \(r_v(x, k)\) for the weights \(w\) and means \(\mu\).

theorem resp_eq_softAssign (θ : ValidParams d K) {v : ℝ} (hv : ∀ k, (θ.1.var k : ℝ) = v)
    (x : EuclideanSpace ℝ (Fin d)) (k : Fin K) :
    resp θ x k = softAssign θ.1.weight θ.1.mean v x k

Uses 8 · Used by 1

Statement usesParameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · Responsibilities in an isotropic Gaussian mixture · Responsibilities with a common variance

Proof usesMarginal of a latent-variable model · Isotropic Gaussian density · Joint density of an isotropic Gaussian mixture

Used byThe Gaussian-mixture M-step mean is the common-variance M-step mean

TheoremRatio of isotropic Gaussian densities with a common variance#✓fully proved

For all points \(\mu, \nu, x \in \mathbb{R}^d\) and every real \(v > 0\), writing \(\mathcal{N}(x \mid \mu, vI)\) for the isotropic Gaussian density with mean \(\mu\) and covariance \(vI\),

\[ \frac{\mathcal{N}(x \mid \mu, vI)}{\mathcal{N}(x \mid \nu, vI)} = \exp\left(\frac{\|x - \nu\|^2 - \|x - \mu\|^2}{2v}\right). \]

theorem isoGaussPDF_div (μ ν x : EuclideanSpace ℝ (Fin d)) {v : ℝ} (hv : 0 < v) :
    isoGaussPDF μ v.toNNReal x / isoGaussPDF ν v.toNNReal x =
      exp ((‖x - ν‖ ^ 2 - ‖x - μ‖ ^ 2) / (2 * v))

Uses 2 · Used by 1

Statement usesIsotropic Gaussian density

Proof usesLog-density of the isotropic Gaussian

Used byCommon-variance responsibilities relative to a fixed component

TheoremExponential decay as the variance tends to zero#✓fully proved

For every real \(c < 0\), \(\exp(c / (2v)) \to 0\) as \(v \to 0^+\).

theorem tendsto_exp_div_nhdsGT_zero {c : ℝ} (hc : c < 0) :
    Tendsto (fun v : ℝ => exp (c / (2 * v))) (𝓝[>] 0) (𝓝 0)

Used by 1

Used byResponsibilities in the zero-variance limit

TheoremCommon-variance responsibilities relative to a fixed component#✓fully proved

For weights \(w_1, \dots, w_K \in \mathbb{R}\), means \(\mu_1, \dots, \mu_K \in \mathbb{R}^d\), a real \(v > 0\), a point \(x \in \mathbb{R}^d\) and components \(j\) and \(k\), the common-variance responsibility \(r_v(x, k)\) of component \(k\) at \(x\) for these weights and means satisfies

\[ r_v(x, k) = \frac{w_k \exp\bigl((\|x - \mu_j\|^2 - \|x - \mu_k\|^2) / (2v)\bigr)} {\sum_i w_i \exp\bigl((\|x - \mu_j\|^2 - \|x - \mu_i\|^2) / (2v)\bigr)}. \]

theorem softAssign_eq (w : Fin K → ℝ) (μ : Fin K → EuclideanSpace ℝ (Fin d)) {v : ℝ} (hv : 0 < v)
    (x : EuclideanSpace ℝ (Fin d)) (j k : Fin K) :
    softAssign w μ v x k = w k * exp ((‖x - μ j‖ ^ 2 - ‖x - μ k‖ ^ 2) / (2 * v)) /
      ∑ i, w i * exp ((‖x - μ j‖ ^ 2 - ‖x - μ i‖ ^ 2) / (2 * v))

Uses 3 · Used by 1

Statement usesResponsibilities with a common variance

Proof usesIsotropic Gaussian density · Ratio of isotropic Gaussian densities with a common variance

Used byResponsibilities in the zero-variance limit

TheoremResponsibilities in the zero-variance limit#✓fully proved

Let \(w_1, \dots, w_K\) be positive weights, \(\mu_1, \dots, \mu_K \in \mathbb{R}^d\) means and \(x \in \mathbb{R}^d\) a point, and suppose that \(\mu_j\) is the unique nearest mean to \(x\): \(\|x - \mu_j\| < \|x - \mu_k\|\) for every \(k \ne j\). Then for every component \(k\), the common-variance responsibility \(r_v(x, k)\) of \(k\) at \(x\) for these weights and means tends to \(1\) if \(k = j\) and to \(0\) otherwise as \(v \to 0^+\).

theorem tendsto_softAssign {w : Fin K → ℝ} (hw : ∀ k, 0 < w k)
    (μ : Fin K → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) {j : Fin K}
    (hj : ∀ k, k ≠ j → ‖x - μ j‖ < ‖x - μ k‖) (k : Fin K) :
    Tendsto (fun v : ℝ => softAssign w μ v x k) (𝓝[>] 0) (𝓝 (if k = j then 1 else 0))

Sources

• Bishop, Pattern Recognition and Machine Learning, Section 9.3.2.

Uses 3 · Used by 2

Statement usesResponsibilities with a common variance

Proof usesCommon-variance responsibilities relative to a fixed component · Exponential decay as the variance tends to zero

Used byThe k-means assignment step is the zero-variance limit of the E-step · The M-step in the zero-variance limit

TheoremThe k-means assignment step is the zero-variance limit of the E-step#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\), let \(\mu_1, \dots, \mu_K \in \mathbb{R}^d\) be means with positive weights \(w_1, \dots, w_K\), and let \(a\) assign to each \(n\) a component \(a(n)\) such that \(\|x_n - \mu_{a(n)}\| < \|x_n - \mu_k\|\) for every \(k \ne a(n)\). Then \(a\) is a nearest-center assignment, that is, \(\|x_n - \mu_{a(n)}\| \le \|x_n - \mu_k\|\) for all \(n\) and \(k\), and for all \(n\) and \(k\) the common-variance responsibility \(r_v(x_n, k)\) of component \(k\) at \(x_n\) for these weights and means tends to \(1\) if \(k = a(n)\) and to \(0\) otherwise as \(v \to 0^+\).

theorem nearest_and_tendsto_softAssign {N : ℕ} (xs : Fin N → EuclideanSpace ℝ (Fin d))
    {w : Fin K → ℝ} (hw : ∀ k, 0 < w k) (μ : Fin K → EuclideanSpace ℝ (Fin d)) (a : Fin N → Fin K)
    (ha : ∀ n k, k ≠ a n → ‖xs n - μ (a n)‖ < ‖xs n - μ k‖) :
    KMeans.Nearest xs μ a ∧ ∀ n k, Tendsto (fun v : ℝ => softAssign w μ v (xs n) k) (𝓝[>] 0)
      (𝓝 (if k = a n then 1 else 0))

Uses 3

Statement usesNearest-center assignment · Responsibilities with a common variance

Proof usesResponsibilities in the zero-variance limit

DefinitionCommon-variance M-step mean#✓fully proved

Given weights \(w_1, \dots, w_K \in \mathbb{R}\), means \(\mu_1, \dots, \mu_K \in \mathbb{R}^d\), a real \(v\) and data \(x_1, \dots, x_N \in \mathbb{R}^d\), the common-variance M-step mean of component \(k\) is

\[ \Bigl(\sum_n r_v(x_n, k)\Bigr)^{-1} \sum_n r_v(x_n, k) \, x_n, \]

where \(r_v(x, k)\) is the common-variance responsibility of component \(k\) at \(x\) for these weights and means, and \(0^{-1} = 0\).

noncomputable def softMean {N : ℕ} (w : Fin K → ℝ) (μ : Fin K → EuclideanSpace ℝ (Fin d)) (v : ℝ)
    (xs : Fin N → EuclideanSpace ℝ (Fin d)) (k : Fin K) : EuclideanSpace ℝ (Fin d) :=
  (∑ n, softAssign w μ v (xs n) k)⁻¹ • ∑ n, softAssign w μ v (xs n) k • xs n

Uses 1 · Used by 2

Statement usesResponsibilities with a common variance

Used byThe Gaussian-mixture M-step mean is the common-variance M-step mean · The M-step in the zero-variance limit

TheoremThe Gaussian-mixture M-step mean is the common-variance M-step mean#✓fully proved

Let \(\theta\) be valid parameters of an isotropic Gaussian mixture with \(K\) components on \(\mathbb{R}^d\), with weights \(w_k\), means \(\mu_k\) and variances all equal to a real number \(v\). Then for data \(x_1, \dots, x_N \in \mathbb{R}^d\) and every component \(k\), the M-step mean of component \(k\) under \(\theta\) equals the common-variance M-step mean of component \(k\) for the weights \(w\), means \(\mu\), variance \(v\) and data \(x_1, \dots, x_N\).

theorem newMean_eq_softMean {N : ℕ} (xs : Fin N → EuclideanSpace ℝ (Fin d)) (θ : ValidParams d K)
    {v : ℝ} (hv : ∀ k, (θ.1.var k : ℝ) = v) (k : Fin K) :
    newMean xs θ k = softMean θ.1.weight θ.1.mean v xs k

Uses 9

Statement usesParameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · M-step mean update for an isotropic Gaussian mixture · Common-variance M-step mean

Proof usesEffective number of points in an isotropic Gaussian mixture · Responsibilities in an isotropic Gaussian mixture · The Gaussian-mixture responsibilities are the common-variance responsibilities · Responsibilities with a common variance

TheoremThe M-step in the zero-variance limit#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data, let \(\mu_1, \dots, \mu_K \in \mathbb{R}^d\) be means with positive weights \(w_1, \dots, w_K\), and let \(a\) assign to each \(n\) a component \(a(n)\) with \(\|x_n - \mu_{a(n)}\| < \|x_n - \mu_k\|\) for every \(k \ne a(n)\). Then for every component \(k\) such that \(a(n) = k\) for some \(n\), the common-variance M-step mean of component \(k\) for these weights, means and data tends, as \(v \to 0^+\), to the k-means centroid of cluster \(k\) under \(a\), the mean of the points \(x_n\) with \(a(n) = k\).

theorem tendsto_softMean {N : ℕ} (xs : Fin N → EuclideanSpace ℝ (Fin d)) {w : Fin K → ℝ}
    (hw : ∀ k, 0 < w k) (μ : Fin K → EuclideanSpace ℝ (Fin d)) (a : Fin N → Fin K)
    (ha : ∀ n k, k ≠ a n → ‖xs n - μ (a n)‖ < ‖xs n - μ k‖) (k : Fin K) (hk : ∃ n, a n = k) :
    Tendsto (fun v : ℝ => softMean w μ v xs k) (𝓝[>] 0) (𝓝 (KMeans.centers xs a k))

Uses 4

Statement usesThe centroid update step · Common-variance M-step mean

Proof usesResponsibilities with a common variance · Responsibilities in the zero-variance limit

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.