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 is positive semidefinite, dominated by A, and exact when it captures the range

Statement

Let $F \in {R, C}$ , $n \geq 1$ , $s \geq 0$ , $A \in F^{n \times n}$ be Hermitian positive semidefinite, and $S \in F^{n \times s}$ . In the Loewner order, where $B ⪯ C$ means $C - B$ is positive semidefinite, the Nyström approximation in The positive-semidefinite Nyström approximation satisfies $0 ⪯ {\hat{A}}_{n y s} ⪯ A$ . If the sketch captures the range in the sense that $Ran (A S) = Ran (A)$ , then ${\hat{A}}_{n y s} = A$ . Here rank, when used in the proof, means dimension of the range.

Facts & Assumptions

Given: A finite Hermitian positive-semidefinite matrix $A$ and a conformal sketch $S$ .

[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 finite-dimensional positive-semidefinite operator has an orthonormal eigenbasis with nonnegative eigenvalues.

[F3]

A non-negative operator has a unique non-negative square root: $A^{1 / 2}$ is Hermitian positive semidefinite and $(A^{1 / 2})^{2} = A$ .

Proof

1.1F1F3algebra

Put $M = A^{1 / 2}$ and $P = P_{Ran (M S)}$ . By [F1], for every vector $x$ , $x^{*} {\hat{A}}_{n y s} x = ∥ P M x ∥_{2}^{2} \geq 0$ and $x^{*} (A - {\hat{A}}_{n y s}) x = ∥ (I - P) M x ∥_{2}^{2} \geq 0$ . Both matrices are Hermitian, so these quadratic-form inequalities prove $0 ⪯ {\hat{A}}_{n y s} ⪯ A$ .

1.2F2F3algebra

Assume $Ran (A S) = Ran (A)$ . By [F2], choose an orthonormal eigenbasis of $A$ with eigenvalues $λ_{i} \geq 0$ . In that basis the diagonal matrix with entries $\sqrt{λ_{i}}$ is positive semidefinite and squares to $A$ , so it equals $A^{1 / 2}$ by uniqueness [F3]. Thus $A$ and $A^{1 / 2}$ have the same range and the same rank.

2.1givenstep 1.2algebra

Let $B = A^{1 / 2} S$ . Then $Ran (B) \subseteq Ran (A^{1 / 2})$ and $A S = A^{1 / 2} B$ . The assumption gives $rank (A S) = rank (A)$ , while a linear map cannot increase the dimension of a subspace's image, so $rank (A S) \leq rank (B) \leq rank (A^{1 / 2}) = rank (A)$ by step 1.2. The ranks are equal, and the range inclusion therefore yields $Ran (B) = Ran (A^{1 / 2})$ .

3.1F1step 2.1algebra∎

The projection in [F1] is consequently the identity on $Ran (A^{1 / 2})$ . Since $A^{1 / 2} x$ lies in that range for every $x$ , [F1] gives ${\hat{A}}_{n y s} x = A^{1 / 2} A^{1 / 2} x = A x$ for every $x$ . Thus ${\hat{A}}_{n y s} = A$ .

Depends on

Used by

A PSD Nyström residual remains positive semidefinite Example

Dependency tree · two levels

12 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

Per-Gunnar Martinsson and Joel A. Tropp, Randomized Numerical Linear Algebra: Foundations & Algorithms, §14.2 (standard reference, not scraped)
Alex Gittens and Michael W. Mahoney, Revisiting the Nyström Method, §4.1 (standard reference, not scraped)