TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Nyström deterministic spectral residual bound under a full-row-rank leading sketch

Statement

Let $F \in {R, C}$ , $n \geq 1$ , $s \geq 0$ , and let $A \in F^{n \times n}$ be Hermitian positive semidefinite with eigenvalues $λ_{1} \geq \dots \geq λ_{n} \geq 0$ . Let $S \in F^{n \times s}$ , and choose an integer $0 \leq k \leq n$ and an orthonormal eigenbasis $U = (U_{1} U_{2})$ with the first $k$ eigenvectors in $U_{1}$ . Set $Λ_{1} = diag (λ_{1}, \dots, λ_{k})$ , $Λ_{2} = diag (λ_{k + 1}, \dots, λ_{n})$ , $Ω_{1} = U_{1}^{*} S$ , and $Ω_{2} = U_{2}^{*} S$ . Empty blocks have norm zero, $λ_{n + 1} : = 0$ , and the $0 \times s$ matrix has full row rank vacuously. If $Ω_{1}$ has full row rank, then, deterministically,

$∥ A - {\hat{A}}_{n y s} ∥_{2} \leq λ_{k + 1} + ∥ Λ_{2}^{1 / 2} Ω_{2} Ω_{1}^{†} ∥_{2}^{2} .$

Here $∥ M ∥_{2} = \sup_{∥ x ∥_{2} = 1} ∥ M x ∥_{2}$ is the induced Euclidean operator norm. No probability assumption on $S$ is made.

Facts & Assumptions

Given: A finite Hermitian positive-semidefinite $A$ , a conformal sketch $S$ , an eigenvalue split at $k$ , and full row rank of $Ω_{1}$ .

[F1]

Nyström is a square-root orthogonal-projection compression: ${\hat{A}}_{n y s} = A^{1 / 2} P_{Ran (A^{1 / 2} S)} A^{1 / 2}$ .

[F2]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: $A$ has an orthonormal eigenbasis with nonnegative eigenvalues.

[F3]

The Moore-Penrose products are orthogonal projectors: if $Ω_{1}$ has full row rank, then $Ω_{1} Ω_{1}^{†} = I_{k}$ .

[F4]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: every finite-dimensional linear map has a singular value decomposition.

[F5]

The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector: the induced operator norm equals the largest singular value.

[F6]

A non-negative operator has a unique non-negative square root: the positive-semidefinite square root is unique.

Proof

1.1F1F4F5algebra

Put $M = A^{1 / 2}$ , $Y = M S$ , and let $P = P_{Ran (Y)}$ . By [F1], $A - {\hat{A}}_{n y s} = M (I - P) M = X^{*} X$ for $X = (I - P) M$ , since $P$ is self-adjoint and idempotent. A singular value decomposition from [F4] writes $X = U_{X} Σ_{X} V_{X}^{*}$ and $X^{*} X = V_{X} Σ_{X}^{2} V_{X}^{*}$ ; [F5] therefore gives $∥ A - {\hat{A}}_{n y s} ∥_{2} = ∥ X ∥_{2}^{2}$ .

1.2F2F3F6algebra

By [F2], choose an orthonormal eigenbasis $U$ of $A$ . The diagonal matrix whose entries are the nonnegative square roots of its eigenvalues is a positive-semidefinite square root, hence it is $A^{1 / 2}$ by uniqueness [F6]. Thus in this basis, $M = U diag (Λ_{1}^{1 / 2}, Λ_{2}^{1 / 2}) U^{*}$ and $U^{*} Y = [\begin{array}{c} Λ_{1}^{1 / 2} Ω_{1} \\ Λ_{2}^{1 / 2} Ω_{2} \end{array}]$ . For any unit vector $x = U (x_{1}, x_{2})$ , set $c = Ω_{1}^{†} x_{1}$ . Then [F3] gives $Ω_{1} c = x_{1}$ , and $Y c = U [\begin{array}{c} Λ_{1}^{1 / 2} x_{1} \\ Λ_{2}^{1 / 2} Ω_{2} Ω_{1}^{†} x_{1} \end{array}] \in Ran (Y)$ .

2.1step 1.1step 1.2algebra

Orthogonal projection gives the shortest distance to its range, so $∥ (I - P) M x ∥_{2} \leq ∥ M x - Y c ∥_{2} = ∥ Λ_{2}^{1 / 2} (x_{2} - Ω_{2} Ω_{1}^{†} x_{1}) ∥_{2}$ . Write $G = Λ_{2}^{1 / 2} Ω_{2} Ω_{1}^{†}$ and $H = Λ_{2}^{1 / 2}$ . For unit $(x_{1}, x_{2})$ , the last norm is at most $∥ G ∥_{2} ∥ x_{1} ∥_{2} + ∥ H ∥_{2} ∥ x_{2} ∥_{2} \leq (∥ G ∥_{2}^{2} + ∥ H ∥_{2}^{2})^{1 / 2}$ by the scalar Cauchy-Schwarz inequality. Taking the supremum over unit $x$ yields $∥ X ∥_{2}^{2} \leq ∥ G ∥_{2}^{2} + ∥ H ∥_{2}^{2}$ .

3.1F2F5step 1.1step 2.1∎

Since $H$ is diagonal with nonnegative entries, [F2] and [F5] give $∥ H ∥_{2}^{2} = λ_{k + 1}$ , including the declared empty-tail convention. Combine this with step 1.1 and step 2.1 to obtain $∥ A - {\hat{A}}_{n y s} ∥_{2} \leq λ_{k + 1} + ∥ Λ_{2}^{1 / 2} Ω_{2} Ω_{1}^{†} ∥_{2}^{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alex Gittens and Michael W. Mahoney, Revisiting the Nyström Method, Theorem 2 and §4.1.1 (standard reference, not scraped)
Nathan Halko, Per-Gunnar Martinsson, and Joel A. Tropp, Finding Structure with Randomness, Theorem 9.1 (standard reference, not scraped)