(G.6)(iii), p. 46 — for A, B with entries in [0,1], ‖A − B‖²_F ≤ ‖A − B‖₁

Proved

RobustSpecClust.Round.frobSq_le_l1

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

frobenius-normmatrix-normsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $A, B \in \mathbb R^{n\times n}$ have all entries in $[0,1]$ . Then the squared Frobenius norm of their difference is at most its entrywise $\ell_1$ norm:

\|A - B\|_F^2 = \sum_{i,j}(A_{ij}-B_{ij})^2 \;\le\; \sum_{i,j}|A_{ij}-B_{ij}| = \|A - B\|_1 .

Applied to $A = \hat X$ and $B = X^0$ , this is step (iii) of (G.6), which turns the Davis–Kahan bound into a bound in terms of the $\ell_1$ estimation error that Theorem 1 controls.

Preamble

import Mathlib
import Definitions.Def_RobustSpecClust_Round_Setting

Formal statement

namespace RobustSpecClust.Round

theorem frobSq_le_l1 {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℝ)
    (hA : ∀ i j, 0 ≤ A i j ∧ A i j ≤ 1) (hB : ∀ i j, 0 ≤ B i j ∧ B i j ≤ 1) :
    frobSq (A - B) ≤ l1 (A - B) := by sorry

end RobustSpecClust.Round

Source

arXiv:1912.07546v3, Appendix G, proof of Theorem 2, p. 46, (G.6)(iii)

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