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

Best rank-k matrix approximation in Frobenius norm

Statement

Let $A \in F^{m \times n}$ , where $m, n \geq 1$ , have a singular value decomposition $A = \sum_{j = 1}^{q} σ_{j} u_{j} v_{j}^{*}, σ_{1} \geq \dots \geq σ_{q} > 0,$ where $q = rank (A)$ . For an integer $k \geq 0$ , put $A_{k} = \sum_{j = 1}^{\min (k, q)} σ_{j} u_{j} v_{j}^{*}, δ_{k}^{2} = \sum_{j = k + 1}^{q} σ_{j}^{2}$ with an empty sum equal to zero. Then $rank (A_{k}) \leq k$ , $∥ A - A_{k} ∥_{F} = δ_{k}$ , and every matrix $B$ with $rank (B) \leq k$ satisfies $∥ A - B ∥_{F} \geq δ_{k}$ .

Facts & Assumptions

Given: A finite-dimensional real or complex matrix $A$ and a rank budget $k \geq 0$ .

[F1]

Finite tensor arrays and the Frobenius inner product: matrix Frobenius norm is the square root of the sum of squared entry moduli, and rank is the dimension of the column image.

[F2]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: a finite-dimensional real or complex linear map has orthonormal input and output bases in which it acts diagonally with nonnegative singular values.

Proof

1.1givenF1F2algebra

Choose the full output singular-vector basis $u_{1}, \dots, u_{m}$ from an SVD of $A$ , ordered so its first $q$ vectors correspond to the positive singular values in the statement. The SVD sends each positive input singular vector to a nonzero multiple of its corresponding output vector and sends every remaining input basis vector to zero. Thus the image of $A$ is exactly $span (u_{1}, \dots, u_{q})$ , so $q = rank (A)$ by [F1]. If $k \geq q$ , then $A_{k} = A$ and $δ_{k} = 0$ , so the lower bound follows from nonnegativity of the norm. Suppose henceforth that $k < q$ , and let $B$ have rank at most $k$ . Its column image has an orthonormal basis; let $P$ be the orthogonal projection onto that image. Then $P B = B$ , and the columnwise orthogonal decomposition by $P$ and $I - P$ gives $∥ A - B ∥_{F}^{2} \geq ∥ (I - P) (A - B) ∥_{F}^{2} = ∥ (I - P) A ∥_{F}^{2}$ .

2.1givenF1F2step 1.1algebra

Put $a_{j} = ∥ P u_{j} ∥^{2}$ for $1 \leq j \leq q$ . Since $P$ is an orthogonal projection, $0 \leq a_{j} \leq 1$ . Expanding the SVD of $A$ and using orthonormality of $(v_{j})$ gives $∥ (I - P) A ∥_{F}^{2} = \sum_{j = 1}^{q} σ_{j}^{2} (1 - a_{j})$ . If $(w_{ℓ})_{ℓ = 1}^{s}$ is an orthonormal basis of the range of $P$ , then the full output basis from step 1.1 gives $\sum_{j = 1}^{q} a_{j} \leq \sum_{ℓ = 1}^{s} \sum_{j = 1}^{m} ∣ ⟨ w_{ℓ}, u_{j} ⟩ ∣^{2} = s = rank (B) \leq k$ .

3.1step 2.1algebra

Write $λ_{j} = σ_{j}^{2}$ , so $λ_{1} \geq \dots \geq λ_{q} > 0$ . Using $\sum_{j} a_{j} \leq k$ , $0 \leq a_{j} \leq 1$ , and $k < q$ , we obtain $\sum_{j = 1}^{q} λ_{j} a_{j} \leq \sum_{j = 1}^{k} λ_{j} a_{j} + λ_{k + 1} \sum_{j = k + 1}^{q} a_{j} \leq k λ_{k + 1} + \sum_{j = 1}^{k} (λ_{j} - λ_{k + 1}) a_{j} \leq \sum_{j = 1}^{k} λ_{j}$ . Therefore step 2.1 implies $∥ A - B ∥_{F}^{2} \geq \sum_{j = k + 1}^{q} σ_{j}^{2} = δ_{k}^{2}$ .

4.1F1F2step 3.1algebra∎

The image of $A_{k}$ is contained in $span (u_{1}, \dots, u_{\min (k, q)})$ , so its rank is at most $k$ . The omitted SVD terms are pairwise Frobenius-orthogonal rank-one matrices because both singular-vector families are orthonormal; hence $∥ A - A_{k} ∥_{F}^{2} = \sum_{j = k + 1}^{q} σ_{j}^{2} = δ_{k}^{2}$ . Together with step 3.1, this proves the truncation is optimal.

Depends on

Used by

Dependency tree · two levels

7 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

Mi-Song Dupuy, Tensor trains for high-dimensional problems, full lecture notes, Chapter 1, §1.1.1, Theorem 1.1.2 (2026) (standard reference, not scraped)