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

Embedding span(A,b) gives the sketch-and-solve residual factor

Statement

Let $A \in K^{n \times p}$ , $b \in K^{n}$ , and $0 < ε < 1$ . Suppose the particular sketch $S$ used in Rank-aware sketch-and-solve least squares is an $ε$ -subspace embedding for $U = span (Ran (A), {b})$ . If that algorithm returns an exact-arithmetic converged vector $\hat{x}$ , then

∥ A \hat{x} - b ∥_{2}^{2} \leq \frac{1 + ε}{1 - ε} \min_{x \in K^{p}} ∥ A x - b ∥_{2}^{2} .

Embedding $Ran (A)$ alone is not a hypothesis for this conclusion.

Facts & Assumptions

Given: Finite $A, b$ , $0 < ε < 1$ , an $ε$ -embedding $S$ of $U = span (Ran (A), {b})$ , and an exact converged output $\hat{x}$ .

[F1]

Every vector in $U$ has its squared norm multiplied by a factor in $[1 - ε, 1 + ε]$ by $S$ (Oblivious squared-norm subspace embeddings).

[F2]

On the stated converged branch, $\hat{x}$ minimizes $∥ S A x - S b ∥_{2}$ over all $x$ (A converged exact sketch-and-solve run returns a sketch minimizer).

[F3]

A least-squares minimizer exists for a linear map between finite-dimensional inner-product spaces (For a linear map $T : V \to W$ between finite-dimensional inner-product spaces, $x$ minimises $∥ T x - b ∥$ if and only if $T^{*} (T x - b) = 0$ , equivalently $T^{*} T x = T^{*} b$ ; minimisers exist and any two differ by an element of $\ker T$ ).

Proof

Given: The hypotheses in the Statement.

1.1F3choose

By [F3], choose an original least-squares minimizer $x_{*} \in K^{p}$ , and write $r_{*} = A x_{*} - b$ , $\hat{r} = A \hat{x} - b$ .

2.1givenF1step 1.1algebra

For every $x \in K^{p}$ , both $A x$ and $b$ belong to $U$ , so their difference $A x - b$ belongs to $U$ . In particular [F1] applies to $\hat{r}$ and $r_{*}$ .

2.2F2step 1.1algebra

By [F2], $\hat{x}$ minimizes the sketched residual, so $∥ S \hat{r} ∥_{2}^{2} \leq ∥ S r_{*} ∥_{2}^{2}$ ; squaring preserves order because both residual norms are nonnegative.

3.1F1step 2.1

The lower inequality in [F1] gives $(1 - ε) ∥ \hat{r} ∥_{2}^{2} \leq ∥ S \hat{r} ∥_{2}^{2}$ .

3.2F1step 2.1

The upper inequality in [F1] gives $∥ S r_{*} ∥_{2}^{2} \leq (1 + ε) ∥ r_{*} ∥_{2}^{2}$ .

4.1step 3.1step 2.2step 3.2step 1.1algebra∎

Combining steps 3.1, 2.2 and 3.2 and dividing by $1 - ε > 0$ proves the claimed estimate, since $x_{*}$ is an original minimizer by step 1.1.

Depends on

Used by

An exact two-row sketch for a three-row regression problem Example

Dependency tree · two levels

9 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

David P. Woodruff, Sketching as a Tool for Numerical Linear Algebra, §2.5, Theorem 21 (standard reference, not scraped)
Michael W. Mahoney, Randomized Algorithms for Matrices and Data, §4.2 (standard reference, not scraped)