TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Frobenius projection onto the positive-semidefinite cone is spectral clipping

Statement

Let $d \geq 1$ and let $A \in R^{d \times d}$ be symmetric. There exists an orthogonal eigendecomposition $A = U diag (λ_{1}, \dots, λ_{d}) U^{T}$ . For any such decomposition define $λ_{i}^{+} = \max {λ_{i}, 0}$ and $A_{+} = U diag (λ_{1}^{+}, \dots, λ_{d}^{+}) U^{T}$ . Let $S_{+}^{d}$ be the set of real symmetric matrices $Z$ with $v^{T} Z v \geq 0$ for every $v \in R^{d}$ , and let $∥ B ∥_{F} = (\sum_{i, j} B_{i j}^{2})^{1 / 2}$ . Then $A_{+}$ is the unique minimizer of $∥ A - Z ∥_{F}$ over $Z \in S_{+}^{d}$ , so its value is independent of the chosen orthogonal eigendecomposition.

Statement references

Real spectral theorem

Nonnegative operators and nonnegative eigenvalues

Positive semidefinite forms and operators over the reals

Orthogonal invariance of the Frobenius norm

Entry-sum Frobenius norm

Higham, §2, Theorem 2.1, article pp. 105–106

Bindel, §6, PDF p. 5

Weinberger and Saul, Appendix A.2, printed p. 240

Facts & Assumptions

Given: A real symmetric matrix $A \in R^{d \times d}$ , $d \geq 1$ , and its orthogonal eigendecomposition from the Statement.

[F1]

Every self-adjoint endomorphism of a finite-dimensional real inner-product space has an orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

[F2]

A self-adjoint operator is nonnegative exactly when its eigenvalues are nonnegative (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).

[F3]

For a finite-dimensional real inner-product space, a self-adjoint operator is nonnegative exactly when its associated symmetric form is positive semidefinite (Over the reals, non-negative and positive operators correspond exactly to positive semidefinite and positive definite symmetric forms).

[F4]

Orthogonal multiplication on either side preserves the Frobenius norm (Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

[F5]

The squared Frobenius norm is the sum of the squares of all matrix entries (The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices).

Proof

1.1F1F2F3given

By [F1], choose an orthogonal eigendecomposition of $A$ and define $A_{+}$ as in the Statement. It is symmetric and has eigenvalues $λ_{i}^{+} \geq 0$ . By [F2] its associated operator is nonnegative, and by [F3] its quadratic form is positive semidefinite; hence $A_{+} \in S_{+}^{d}$ .

1.2F4given

Let $Z \in S_{+}^{d}$ and set $W = U^{T} Z U$ . For each coordinate vector $e_{i}$ , $W_{i i} = e_{i}^{T} W e_{i} = (U e_{i})^{T} Z (U e_{i}) \geq 0$ ; also $W$ is symmetric. Orthogonal invariance [F4] gives $∥ A - Z ∥_{F}^{2} = ∥ diag (λ_{1}, \dots, λ_{d}) - W ∥_{F}^{2}$ .

2.1step 1.2F5algebra

Expanding the entry sum [F5], the last square is $\sum_{i} (λ_{i} - W_{i i})^{2} + \sum_{i \neq j} W_{i j}^{2}$ . For every $w \geq 0$ , $(λ_{i} - w)^{2} \geq (λ_{i} - λ_{i}^{+})^{2}$ : if $λ_{i} \geq 0$ the right side is zero and equality is attained only at $w = λ_{i}$ , while if $λ_{i} < 0$ then $w - λ_{i} \geq - λ_{i}$ and equality is attained only at $w = 0$ . Thus every feasible $Z$ has squared distance at least $\sum_{i} (λ_{i} - λ_{i}^{+})^{2}$ .

3.1step 2.1givenalgebra

For $Z = A_{+}$ the conjugated matrix $W$ is $diag (λ_{1}^{+}, \dots, λ_{d}^{+})$ , so all off-diagonal terms vanish and every diagonal term attains its lower bound from step 2.1. Hence $A_{+}$ is a minimizer.

4.1step 2.1step 3.1algebra∎

Equality in the lower bound requires every off-diagonal square in step 2.1 to vanish and every diagonal term to attain its unique scalar minimum. Therefore $W = diag (λ_{1}^{+}, \dots, λ_{d}^{+})$ and $Z = U W U^{T} = A_{+}$ . The minimizer is unique; since the argument applies to any orthogonal eigendecomposition, every allowed decomposition gives this same nearest matrix.

Remarks

The proof above is choice-free: it constructs the unique minimizer from a finite orthogonal eigendecomposition and checks the objective directly. The separate abstract Hilbert-projection route used in the LMNN procedure is recorded under its own Countable Choice assumption.

Depends on

Used by

Dependency tree · two levels

26 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

Nicholas J. Higham, Computing a Nearest Symmetric Positive Semidefinite Matrix, Linear Algebra and its Applications 103 (1988), 103–118 (standard reference, not scraped)
David Bindel, Matrix Computations, CS 6210, Matrix Nearness Problems, Fall 2022 (standard reference, not scraped)
Kilian Q. Weinberger and Lawrence K. Saul, Distance Metric Learning for Large Margin Nearest Neighbor Classification, JMLR 10 (2009), 207–244 (standard reference, not scraped)