Proof of Theorem 2, p. 47 — for B* = Diag(1/√n_k)O with O orthogonal, ‖b_l − b_k‖ = √(1/n_k + 1/n_l)

Proved

RobustSpecClust.Round.bstar_sep

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

orthogonal-matrixp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1spectral-clustering

Let $\varphi : [n]\to[r]$ be a labelling with all cluster sizes $n_k > 0$ , let $O \in \mathbb R^{r\times r}$ be orthogonal and $B^* = \mathrm{Diag}(1/\sqrt{n_1},\dots,1/\sqrt{n_r})\,O$ with rows $b^*_1,\dots,b^*_r$ . Then for all $k \ne l$ ,

\|b^*_l - b^*_k\| = \sqrt{\frac1{n_k} + \frac1{n_l}} .

In particular $\delta_k = 1/\sqrt{n_k}$ satisfies $\delta_k \le \min_{l \ne k}\|b^*_l - b^*_k\|$ , the hypothesis of Lemma 5, so that $|\mathcal S_k|\delta_k^2 = |\mathcal S_k|/n_k$ in Theorem 2. Note $U^0 O = \Theta(\varphi)B^*$ , so $V = U^0O$ is k-means feasible.

Preamble

import Mathlib
import Definitions.Def_RobustSpecClust_Round_Setting

Formal statement

namespace RobustSpecClust.Round

open Matrix

theorem bstar_sep {n r : ℕ} (φ : Fin n → Fin r) (hφ : ∀ k, 0 < clusterSize φ k)
    (O : Matrix (Fin r) (Fin r) ℝ) (hO : O ∈ Matrix.orthogonalGroup (Fin r) ℝ)
    (k l : Fin r) (hkl : k ≠ l) :
    vecNorm ((Matrix.diagonal (fun j => 1 / Real.sqrt (clusterSize φ j)) * O) l -
        (Matrix.diagonal (fun j => 1 / Real.sqrt (clusterSize φ j)) * O) k)
      = Real.sqrt (1 / (clusterSize φ k : ℝ) + 1 / (clusterSize φ l : ℝ)) := by sorry

end RobustSpecClust.Round

Source

arXiv:1912.07546v3, Appendix G, proof of Theorem 2, p. 47, first paragraph ("‖b*_l − b*_k‖ = √(1/n_k + 1/n_l)")

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proof of Theorem 2, p. 47 — for B* = Diag(1/√n_k)O with O orthogonal, ‖b*_l − b*_k‖ = √(1/n_k + 1/n_l)

Proof of Theorem 2, p. 47 — for B* = Diag(1/√n_k)O with O orthogonal, ‖b_l − b_k‖ = √(1/n_k + 1/n_l)