TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

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.

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison

Statement

Let $F$ be $R$ or $C$ , let $A \in M_{m \times n} (F)$ , and let $σ_{1} \geq σ_{2} \geq \dots \geq σ_{r} > 0$ be the positive singular values of $A$ , where $r = rank A$ ; write $σ_{1} = 0$ when $r = 0$ .

Spectral formula. $∥ A ∥_{2} = σ_{1}$ , where $∥ \cdot ∥_{2}$ is the operator norm of The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||.
Frobenius formula. $∥ A ∥_{F} = (σ_{1}^{2} + \dots + σ_{r}^{2})^{1 / 2}$ .
Unitary invariance. For every unitary $U \in M_{m} (F)$ and $V \in M_{n} (F)$ (over $F = R$ : orthogonal matrices), $∥ U A V ∥_{2} = ∥ A ∥_{2}, ∥ U A V ∥_{F} = ∥ A ∥_{F} .$
Sharp rank comparison. $∥ A ∥_{2} \leq ∥ A ∥_{F} \leq \sqrt{r} ∥ A ∥_{2} .$ The lower inequality is an equality exactly when $r \leq 1$ ; the upper inequality is an equality exactly when $σ_{1} = \dots = σ_{r}$ , that is, when all nonzero singular values coincide. In particular $∥ A ∥_{F} \leq \sqrt{\min (m, n)} ∥ A ∥_{2}$ .

Facts & Assumptions

Given: A matrix $A \in M_{m \times n} (F)$ over $F = R$ or $C$ , with singular values $σ_{1} \geq \dots \geq σ_{r} > 0$ .

[L1]

There is a singular value decomposition $A = U Σ V^{*}$ with $U, V$ unitary (orthogonal over $R$ ) and $Σ$ the diagonal matrix of the singular values (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition).

[L2]

The operator norm of a map between finite-dimensional real or complex inner product spaces equals its largest singular value (The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector).

[L3]

The rank of a linear map is the number of its positive singular values (The rank of a linear map is the number of its nonzero singular values).

[L4]

A unitary (orthogonal) operator preserves norms: $∥ Q v ∥ = ∥ v ∥$ for every vector $v$ (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces).

[L5]

Compositions and adjoints of unitary operators are unitary (Orthogonal and unitary operators form groups, and their determinants have modulus one).

Proof

technique · direct

1.1L2

Claim 1 is [L2] applied to the map $x \mapsto A x$ : $∥ A ∥_{2} = σ_{1}$ .

1.2L4algebra

Left invariance of the Frobenius norm. For unitary $Q \in M_{m} (F)$ , each column of $Q A$ is the image under $Q$ of the corresponding column of $A$ , so by [L4] $∥ (Q A) column j ∥_{2} = ∥ A column j ∥_{2}$ for every $j < n$ ; summing over $j$ gives $∥ Q A ∥_{F}^{2} = \sum_{j < n} ∥ (Q A)_{j} ∥_{2}^{2} = \sum_{j < n} ∥ A_{j} ∥_{2}^{2} = ∥ A ∥_{F}^{2}$ , using the entry formula of The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices.

1.3L4algebra

Right invariance of the Frobenius norm. For unitary $Z \in M_{n} (F)$ , the $i$ -th row of $A Z$ is ${row}_{i} (A) Z$ , and by [L4] applied to $Z^{*}$ , $∥ {row}_{i} (A) Z ∥_{2} = ∥ {row}_{i} (A) ∥_{2}$ for every $i < m$ ; summing over $i$ gives $∥ A Z ∥_{F}^{2} = \sum_{i < m} ∥ {row}_{i} (A) ∥_{2}^{2} = ∥ A ∥_{F}^{2}$ .

1.4L1L5algebra

Singular values of $U A V$ . If $A = U_{0} Σ V_{0}^{*}$ is the decomposition of [L1], then $U A V = (U U_{0}) Σ (V^{*} V_{0}) = (U U_{0}) Σ (V_{0}^{*} V)^{*}$ , and by [L5] the factors $U U_{0}$ and $V_{0}^{*} V$ are unitary, so this is a singular value decomposition of $U A V$ with the same singular values as $A$ .

2.1L1step 1.2step 1.3algebra

From [L1], $A = U Σ V^{*}$ , so steps 1.2 and 1.3 give $∥ A ∥_{F}^{2} = ∥ U Σ V^{*} ∥_{F}^{2} = ∥ Σ ∥_{F}^{2}$ , and the diagonal entries of $Σ$ are $σ_{1}, \dots, σ_{r}$ followed by zeros, so $∥ Σ ∥_{F}^{2} = σ_{1}^{2} + \dots + σ_{r}^{2}$ by the entry formula of The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices. This is claim 2.

3.1step 1.4step 1.1step 2.1

Claim 3 follows: by step 1.4 the singular values of $U A V$ are those of $A$ , so claim 1 gives $∥ U A V ∥_{2} = σ_{1} = ∥ A ∥_{2}$ and claim 2 gives $∥ U A V ∥_{F} = (\sum_{j} σ_{j}^{2})^{1 / 2} = ∥ A ∥_{F}$ .

3.2step 1.1step 2.1L3algebra

The lower inequality. The maximum $σ_{1}$ is at most the Euclidean total $(σ_{1}^{2} + \dots + σ_{r}^{2})^{1 / 2}$ , each term being nonnegative, so claims 1 and 2 give $∥ A ∥_{2} \leq ∥ A ∥_{F}$ . Equality holds exactly when $σ_{2} = \dots = σ_{r} = 0$ , that is exactly when $r \leq 1$ by [L3].

3.3step 1.1step 2.1algebra

The upper inequality. Each $σ_{j} \leq σ_{1}$ , so $σ_{1}^{2} + \dots + σ_{r}^{2} \leq r σ_{1}^{2}$ , and claims 1 and 2 give $∥ A ∥_{F} \leq \sqrt{r} σ_{1} = \sqrt{r} ∥ A ∥_{2}$ . Equality holds exactly when $\sum_{j \leq r} (σ_{1}^{2} - σ_{j}^{2}) = 0$ , a sum of nonnegative terms, hence exactly when every $σ_{j} = σ_{1}$ .

4.1step 3.3L3

Since $r \leq \min (m, n)$ by [L3], the upper bound also gives $∥ A ∥_{F} \leq \sqrt{\min (m, n)} ∥ A ∥_{2}$ .

5.1step 1.1step 2.1step 3.1step 3.2step 3.3step 4.1∎

Claims 1, 2, 3 and 4 are steps 1.1, 2.1, 3.1 and steps 3.2, 3.3 and 4.1.

Depends on

Used by

Dependency tree · two levels

25 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 Bindel, CS 6210: Matrix Nearness Problems (standard reference, not scraped)
L. N. Trefethen and D. Bau III, Numerical Linear Algebra, Lecture 3 (standard reference, not scraped)