Lemma 22.1: an iteration of the k-means algorithm (reassign to nearest centroids, recompute centroids) does not increase the k-means objective

Proved

UnderstandingML.kmeans_step_nonincreasing

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-meanslloyd-algorithmmonotonicity

Lemma 22.1. Each iteration of the k-means algorithm does not increase the k-means objective function (as given in Equation (22.1)).

Formally: if $C^{(t-1)}$ and $C^{(t)}$ are partitions of the data $X \subseteq \mathbb{R}^n$ into $k$ clusters and $C^{(t)}$ assigns every point to a nearest centroid $\mu(C^{(t-1)}_i)$ (ties arbitrary), then $G(C^{(t)}) \le G(C^{(t-1)})$ .

Preamble

import Definitions.Def_UnderstandingML_Clustering

open MeasureTheory

Formal statement

namespace UnderstandingML

/-- **Lemma 22.1** (p. 313). Each iteration of the k-means algorithm does not increase the
k-means objective function (as given in Equation (22.1)): if `C⁽ᵗ⁾` assigns every point of `X`
to a nearest centroid of the previous partition `C⁽ᵗ⁻¹⁾`, then `G(C⁽ᵗ⁾) ≤ G(C⁽ᵗ⁻¹⁾)`. -/
theorem kmeans_step_nonincreasing {n k : ℕ} (S : Finset (Vec n)) (C C' : Fin k → Finset (Vec n))
    (hC : IsPartition S C) (hC' : IsPartition S C')
    (hnear : IsNearestAssignment (fun i ↦ centroid (C i)) C') :
    kmeansObjective C' ≤ kmeansObjective C := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §22.2.1 pp. 313-314, Lemma 22.1 with its proof

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph