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.
The Hilbert orthogonal projection onto a closed subspace
Definition
Assume the Axiom of Countable Choice. Let be a closed linear subspace of a real or complex Hilbert space (Linear subspace of a vector space). By the orthogonal-decomposition theorem (Orthogonal decomposition by a closed subspace) every has a unique representation
and the Hilbert orthogonal projection onto is the map
assigning to its unique -component. Its defining properties are therefore
which characterise uniquely: a map with these defining properties must agree with the -component of the unique decomposition of each .
Agreement with the finite-dimensional projection. If is a finite-dimensional inner-product space and a subspace, then For a subspace of a finite-dimensional inner product space, writes and The orthogonal projection is the -component in defines as the unique -component of ; the defining properties displayed above are the same, so they define the same map on a finite-dimensional Hilbert space.
Range and kernel. for every , and for because with ; conversely says exactly that . Hence the range of is and its kernel is , and is the identity on and zero on .
Depends on
Used by
- Continuous calculus does not contain discontinuous spectral projections Counterexample
- Isometry coisometry and partial isometry Definition
- Projection valued measure Definition
- Distance to a closed subspace Example
- Polar decomposition of the unilateral shift Example
- Projection onto a finite-dimensional subspace by a Gram matrix Example
- Projection onto the constants is the mean Example
- Hilbert projections are linear, self-adjoint and contractive Lemma
- Maximal orthogonal family of cyclic reducing subspaces Lemma
- Agreement with the concrete L-two projection Remark
- Partial isometry characterizations Theorem
- Polar decomposition for bounded operators Theorem
- Toeplitz hausdorff Theorem
Dependency tree · two levels
22 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
- Theo Bühler and Dietmar Salamon, Functional Analysis, Definition 5.36, p.237 (standard reference, not scraped)
- Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, Definition 182 and Proposition 183 (standard reference, not scraped)