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.
Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis
Statement
Let be a finite-dimensional real inner product space and let be self-adjoint. Then has an orthonormal basis consisting of eigenvectors of .
Facts & Assumptions
Given: A finite-dimensional real inner product space and a self-adjoint endomorphism .
Every self-adjoint endomorphism is normal (Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space).
A real normal endomorphism admits an orthonormal block decomposition by real blocks and blocks (A real normal endomorphism is orthogonally block-diagonalisable with 1x1 real blocks and 2x2 rotation-scaling blocks).
In an orthonormal basis, self-adjointness means symmetry of the matrix (In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose).
Proof
By [L1] and [L2], there is an orthonormal basis in which the matrix of is block diagonal with real blocks and blocks .
Because is self-adjoint, [L3] says that the same matrix is symmetric. A block above is symmetric exactly when , so every block collapses to the scalar block . Therefore the whole matrix is diagonal.
A diagonal matrix acts on each basis vector by scalar multiplication, so the orthonormal basis from step 2.1 is an orthonormal eigenbasis of .
Depends on
- Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space
- In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose
- A real normal endomorphism is orthogonally block-diagonalisable with 1x1 real blocks and 2x2 rotation-scaling blocks
Used by
- An explicit real symmetric 3x3 matrix is orthogonally diagonalised Example
- The non-negative square root of an explicit matrix is exhibited as a polynomial in the matrix Example
- 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 Theorem
- Courant-Fischer min-max principle for self-adjoint endomorphisms on finite-dimensional real inner product spaces Theorem
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
- Sheldon Axler, Linear Algebra Done Right, fourth edition (standard reference, not scraped)