TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Projected CUR has a two-sided Frobenius residual bound

Statement

Let $F \in {R, C}$ , $m, n \geq 1$ , $A \in F^{m \times n}$ , and choose an integer $0 \leq k \leq \min (m, n)$ and ordered lists $I, J$ of $k$ distinct valid row and column indices, respectively. Set $C = A (:, J)$ and $R = A (I, :)$ as in Skeleton and projected least-squares CUR cores, and define $P_{C} = C C^{†}$ and $P_{R} = R^{†} R$ . The projected least-squares CUR approximation is ${\hat{A}}_{p r o j} = C (C^{†} A R^{†}) R = P_{C} A P_{R}$ . With $∥ X ∥_{F} = (\sum_{i, j} ∣ X_{i j} ∣^{2})^{1 / 2}$ ,

$∥ A - {\hat{A}}_{p r o j} ∥_{F} \leq ∥ (I_{m} - P_{C}) A ∥_{F} + ∥ A (I_{n} - P_{R}) ∥_{F} .$

This bound is for the projected least-squares core only; it is not asserted for the skeleton core $W^{†}$ .

Facts & Assumptions

Given: A finite real or complex matrix $A$ , selected matrices $C, R$ , and their unique Moore-Penrose inverses.

[F1]

Skeleton and projected least-squares CUR cores: the projected core is $C^{†} A R^{†}$ and its reconstruction is $(C C^{†}) A (R^{†} R)$ .

[F2]

The Moore-Penrose products are orthogonal projectors: $C C^{†}$ and $R^{†} R$ are orthogonal projections.

Proof

1.1F1F2given

Put $P_{C} = C C^{†}$ and $P_{R} = R^{†} R$ . By [F1], ${\hat{A}}_{p r o j} = P_{C} A P_{R}$ , and [F2] makes both factors orthogonal projections.

2.1step 1.1algebra

Algebra gives $A - P_{C} A P_{R} = (I_{m} - P_{C}) A + P_{C} A (I_{n} - P_{R})$ .

3.1step 1.1step 2.1algebra∎

For an orthogonal projection $P$ and each column vector $x$ , the decomposition $x = P x + (I - P) x$ is orthogonal, so $∥ P x ∥_{2} \leq ∥ x ∥_{2}$ . Summing squared column norms gives $∥ P Y ∥_{F} \leq ∥ Y ∥_{F}$ for every compatible matrix $Y$ . The Frobenius norm is the Euclidean norm of the entries, so its triangle inequality applied to step 2.1 and this contraction with $P = P_{C}$ , $Y = A (I_{n} - P_{R})$ gives the asserted bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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, §13.2 (standard reference, not scraped)
Nathan Halko, Per-Gunnar Martinsson, and Joel A. Tropp, Finding Structure with Randomness, §3.2.3 (standard reference, not scraped)