Alphabeta MathHow 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.
Rank-r orthogonal projector domain
Definition
Let and let be an integer with . Use Hermitian adjoints and matrices as in Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space and Rectangular matrix multiplication and the identity matrix , including zero-sized shapes, trace as in The trace as the sum of the diagonal entries, and the Frobenius norm as in The Frobenius norm on real or complex matrices. Write for the real vector space of Hermitian matrices, with Frobenius inner product The rank- orthogonal projector domain is An element of is an orthogonal projector; its range is the occupied subspace. The statement that its range has dimension is justified by A Hermitian idempotent has trace equal to its rank ↗. A frame with represents ; replacing by for a unitary leaves unchanged.
Depends on
- Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
- The trace $\operatorname{tr}(A)$ as the sum of the diagonal entries
- The Frobenius norm $\lVert A\rVert_F=(\sum_{i,j}|a_{ij}|^2)^{1/2}$ on real or complex matrices
Used by
- Finite-basis projector energy model Definition
- The fixed-particle admissible Hermitian density domain Definition
- The occupied-projector response map on its strict-gap domain Definition
- A cusp in a chosen exchange-correlation term violates the C2 hypothesis Example
- A two-level nonlinear projector model has a stationary strict maximum Example
- A Hermitian idempotent has trace equal to its rank Lemma
- A spectral gap persists on a computable matrix ball with a uniform resolvent bound Lemma
- A strict occupied gap defines a unique rank-r spectral projector Lemma
- Complex projector tangents are skew-Hermitian commutator directions Lemma
- Density mixing preserves admissibility but need not preserve idempotence Lemma
- Every rank-r orthogonal projector is an admissible density Lemma
- Graph charts and tangent directions for complex rank-r projectors Lemma
- The finite rank-r projector domain is nonempty and compact Lemma
- A level shift preserves a fixed occupied projector exactly under block ordering Theorem
- A separated block spectral projector is Frechet differentiable with a resolvent bound Theorem
Dependency tree · two levels
12 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
- Alan Edelman, Tomás A. Arias, and Steven T. Smith, The Geometry of Algorithms with Orthogonality Constraints, SIAM Journal on Matrix Analysis and Applications 20 (1998), §§2.3.2 and 2.5 (standard reference, not scraped)
- P.-A. Absil, R. Mahony, and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Chapter 3, Princeton University Press (2008), §§3.4.4–3.6 (standard reference, not scraped)