LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The weighted centroid minimizes finite-cluster squared error

Statement

Let $x_{1}, \dots, x_{N} \in R^{d}$ , let $w_{i} > 0$ with $\sum_{i = 1}^{N} w_{i} = 1$ , and let $S \subseteq {1, \dots, N}$ be nonempty. Put $W_{S} : = \sum_{i \in S} w_{i}$ and $μ_{S} : = W_{S}^{- 1} \sum_{i \in S} w_{i} x_{i}$ . For every $c \in R^{d}$ ,

$\sum_{i \in S} w_{i} ∥ x_{i} - c ∥_{2}^{2} = \sum_{i \in S} w_{i} ∥ x_{i} - μ_{S} ∥_{2}^{2} + W_{S} ∥ c - μ_{S} ∥_{2}^{2} .$

Consequently, $μ_{S}$ is the unique minimizer of the cluster's weighted squared error. If $S$ is empty, its cost is zero for every center and no centroid is required.

Facts & Assumptions

Given: A finite list of vectors $x_{i} \in R^{d}$ , positive weights summing to one, and a nonempty index set $S$ .

[A1]

The inner product and squared norm on $R^{d}$ are $⟨ x, y ⟩ = \sum_{ℓ = 1}^{d} x_{ℓ} y_{ℓ}$ and $∥ x ∥_{2}^{2} = ⟨ x, x ⟩$ .

Proof

1.1givenA1algebra

Since $S$ is nonempty and each $w_{i} > 0$ , $W_{S} > 0$ , so $μ_{S}$ is defined and $\sum_{i \in S} w_{i} (x_{i} - μ_{S}) = 0$ by its formula.

2.1givenA1step 1.1algebra

Write $x_{i} - c = (x_{i} - μ_{S}) + (μ_{S} - c)$ and expand the squared norm using [A1]. Summing over $S$ , the cross term is $2 ⟨ \sum_{i \in S} w_{i} (x_{i} - μ_{S}), μ_{S} - c ⟩ = 0$ by step 1.1; the remaining terms give the displayed identity.

3.1givenstep 2.1algebra∎

The last term in step 2.1 is nonnegative and vanishes exactly when $c = μ_{S}$ , because $W_{S} > 0$ and a Euclidean squared norm vanishes exactly at the zero vector. Thus $μ_{S}$ uniquely minimizes the cost. For empty $S$ , the sum has no terms and equals zero for every $c$ .

Used by

Exact finite-data Lloyd quantizer Algorithm
Exhaustive global empirical squared-error quantizer Algorithm
Lloyd can stop at a strictly suboptimal finite-data fixed point Counterexample
Exact finite-data Lloyd descent and finite termination Theorem
Exhaustive empirical search attains a global quantizer Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Robert M. Gray, Source Coding Theory, first edition (standard reference, not scraped)
Robert Gallager, 6.450 Principles of Digital Communications I, Chapter 3: Quantization (standard reference, not scraped)
Robert M. Gray and David L. Neuhoff, Quantization, IEEE Transactions on Information Theory 44(6) (1998) (standard reference, not scraped)