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 orthogonal projection is the unique nearest point in the subspace
Statement
Let be a subspace of a finite-dimensional inner product space . For every , the vector is the unique point of nearest to : for every ,
with equality if and only if .
Facts & Assumptions
Given: A subspace , a vector , and .
The residual lies in , while lies in (The orthogonal projection is the -component in ).
Orthogonal vectors satisfy (Pythagoras, the parallelogram identity, and the real and complex polarisation identities).
Proof
Decompose . The first term lies in and the second in , so they are orthogonal by [L1].
By [L2], . Nonnegativity gives the asserted inequality.
Equality holds exactly when , which by positive definiteness is exactly .
Depends on
Used by
- Projection onto a plane in ℝ³ and the nearest-point calculation Example
- ‖ v‖₂ d(w,ℝv)=|det[v w]| for v≠0 in ℝ² Lemma
- For a linear map T:V→ W between finite-dimensional inner-product spaces, x minimises ‖ Tx-b‖ if and only if T^*(Tx-b)=0, equivalently T^*Tx=T^*b; minimisers exist and any two differ by an element of ker T Theorem
- Near a simple Hermitian eigenvector, Rayleigh-quotient iteration converges cubically Theorem
- Normal equations for best affine L² prediction Theorem
Dependency tree · two levels
5 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, 4th ed., result 6.61 (standard reference, not scraped)
- Sergei Treil, Linear Algebra Done Wrong, Theorem 5.3.2 (standard reference, not scraped)