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.
Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans
Statement
Let be a finite linearly independent list in a real or complex inner product space. There is an orthonormal list such that, for every ,
It is obtained recursively from
For , both lists are empty.
Facts & Assumptions
Given: A finite linearly independent list .
An orthonormal list is orthogonal and every listed vector has norm one (Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases).
A finite list is linearly independent when every list of scalars with has for all (Linear independence: a finite list is independent when forces every , and a subset is independent when every injective finite list into is independent).
For a nonzero vector , positive definiteness gives , so is defined and has norm one (The norm induced by a real or complex inner product).
Every finite orthogonal list of nonzero vectors is linearly independent (Every finite orthogonal list of nonzero vectors is linearly independent).
The span of a set is exactly the vectors obtained as finite linear combinations of its elements, including the empty combination. For a finite list, grouping the finitely many terms by their listed vectors gives a coefficient combination indexed by the list. Every subspace containing those vectors contains these combinations. ( is exactly the set of linear combinations of finite lists of elements of , and )
Proof
For there is nothing to construct, and the successive-span assertion at is equality of zero subspaces.
Suppose have been constructed orthonormally with the required span equalities. Define by the displayed formula. For , linearity and orthonormality give .
If , then lies in , say ; then the scalars for , and for satisfy with , contradicting the independence of through [L2]. Hence , and [L3] makes a unit vector orthogonal to its predecessors.
The formula for shows lies in , while its rearrangement shows lies in . Together with the induction hypothesis these give both inclusions in the span equality at .
Induction constructs the stated list and proves every successive-span equality. Its vectors are nonzero and orthogonal, so [L4] also confirms their independence; their unit norms make the list orthonormal.
Depends on
- Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases
- Every finite orthogonal list of nonzero vectors is linearly independent
- The norm $\lVert v\rVert=\sqrt{\langle v,v\rangle}$ induced by a real or complex inner product
- Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i<n} \lambda_i v_i = 0_V$ forces every $\lambda_i = 0_F$, and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent
- $\operatorname{span}(S)$ is exactly the set of linear combinations of finite lists of elements of $S$, and $\operatorname{span}(\varnothing) = \{0_V\}$
Used by
- Finite-budget stable block reordering for Schur and QZ forms Algorithm
- Every finite-dimensional real or complex inner product space has an orthonormal basis Corollary
- Local formula for distance from the centre of a normal neighbourhood Corollary
- Sufficiently short geodesic segments are uniquely minimizing Corollary
- A conjugate point at which there are many geodesics Counterexample
- Antipodal points on a round sphere have many minimizing geodesics Counterexample
- E-valued Dolbeault operators and their L2 structure Definition
- QR and polar retractions on Stiefel and Grassmann Definition
- The Thom prespectrum of the universal real and oriented bundles Definition
- A worked QR factorisation of an invertible real matrix Example
- Chebyshev extremals and the exact disk Fekete polynomial Example
- Complex finite-basis PC-VAR optimization on Grassmann Example
- Gram–Schmidt on an explicit basis of ℂ² with conjugation visible Example
- Gram–Schmidt on an explicit basis of ℝ³ Example
- Legendre polynomials from Gram–Schmidt Example
- Normal equations square the conditioning compared with QR on a badly scaled least-squares problem Example
- Coherent Johnson row access with stored values Lemma
- Embedded bands joining two framed spheres exist Lemma
- Finite affine bubbles represent signed cubical sums Lemma
- Finite ancilla amplification is a well-defined block map Lemma
- Formal adjoints of differential operators on metric vector bundles Lemma
- Frame fields with prescribed boundary conditions along a clean Whitney disk Lemma
- General linear frame spaces have the Stiefel cohomology gap Lemma
- General linear Stiefel approximations stabilize bounded constructible Hom Lemma
- Global geodesic-polar coordinates from a boundary point on a simple manifold Lemma
- Opposite local signs give the compatible Whitney-circle framing Lemma
- Positive moment Gram matrices produce orthonormal polynomial families Lemma
- Radial geodesics from one point reach every point under global exponential domain Lemma
- Rank-revealing QR sweeps give exact mixed canonical gauge Lemma
- Stably trivial bundles over spheres below the rank are trivial Lemma
- The collapse of an embedded manifold classifies through the universal Thom prespectrum Lemma
- The Whitney framing extends over a clean disk in the stable range Lemma
- Two dimensional numerical range is convex Lemma
- Uniform boundary Schauder bounds and smooth interior domain approximants Lemma
- At a conjugate endpoint the index form is degenerate Proposition
- Orthogonal complements of subbundles are smooth subbundles Proposition
- A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent Theorem
- A real normal endomorphism is orthogonally block-diagonalisable with 1x1 real blocks and 2x2 rotation-scaling blocks Theorem
- A Riemannian manifold is flat iff it is locally isometric to Euclidean space Theorem
- Every invertible real or complex square matrix has a unique factorisation A=QR with Q orthogonal or unitary and R upper triangular with positive real diagonal Theorem
…and 18 more results.
Dependency tree · two levels
19 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.32 (standard reference, not scraped)
- Sergei Treil, Linear Algebra Done Wrong, §5.3.1 (standard reference, not scraped)