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.
Orthonormal families, complete orthonormal systems and Hilbert bases
Definition
Let be a real or complex inner-product space (Real and complex inner-product spaces and their induced length), with inner product linear in the first argument and conjugate-linear in the second, and with the induced length . The definitions below do not require completeness. When the term Hilbert basis is used, is additionally assumed complete (Hilbert space).
Orthonormal indexed family. Let be any set. An indexed family of vectors of is orthonormal when
Because in the scalar field, the family contains no zero vector: , so for every (Real and complex inner-product spaces and their induced length); and the index map is injective, since with would give . Thus an orthonormal family is the same thing as an orthonormal set together with a labelling of it, and in the sequel no choice is hidden in passing between the two descriptions. Orthonormal set. A subset is orthonormal when every has and for all distinct . For such an the family with is orthonormal in the indexed sense, and the image of an orthonormal indexed family is an orthonormal set. Orthogonal means (Orthogonality and the orthogonal complement). Independence and unique coefficients. Let be orthonormal, let be finite, and let scalars satisfy . For each fixed , linearity in the first argument gives
so every finite subfamily of an orthonormal family is linearly independent. In particular the coefficients in a finite expansion are unique: if , then applying the computation to gives for every .
Closed linear span and completeness. The span of an indexed family is the set of all finite linear combinations with finite and scalars ; it is the smallest linear subspace of containing every (Linear subspace of a vector space). Its closure in the induced norm is the closed linear span of the family, the smallest closed linear subspace of containing every . The family is complete, or is a complete orthonormal system, when its closed linear span is all of . A Hilbert basis, or orthonormal basis, of is a complete orthonormal family in .
The empty family. The span of the empty family is , which is already closed, so the empty family is complete exactly when . Thus the zero Hilbert space always has a Hilbert basis, namely the empty one.
Not a Hamel basis, and no order is assumed. A Hilbert basis is a basis only in the sense of closed linear span: for an infinite-dimensional the vectors of are in general not finite linear combinations of a Hilbert basis, and the expansion of an arbitrary vector is a norm limit of finite partial sums, not a finite sum. No enumeration, ordering or countability of the index set is part of the definition; the partial sums are indexed by the finite subsets of , ordered by inclusion, and that is the convention used on this page.
Coefficient notation. For orthonormal and the scalars are the coefficients of with respect to the family. They are well defined for every , without any assumption that the family is complete.
Depends on
Used by
- A separable infinite-dimensional Hilbert space is ℓ² Corollary
- Existence of self-adjoint extensions is equality of deficiency indices Corollary
- Orthonormal eigenbasis for a compact self adjoint operator Corollary
- The unilateral shift obstructs a cyclic linear trace extension Counterexample
- The unilateral shift obstructs a cyclic linear trace extension Counterexample
- Deficiency subspaces and deficiency indices Definition
- Discrete and essential spectrum of a self-adjoint operator Definition
- Hilbert–Schmidt operator and Hilbert–Schmidt norm Definition
- Trace of a trace class operator Definition
- A square-integrable separable product kernel Example
- Diagonal Schatten class criteria on ell two Example
- Finite-rank truncations of a square-integrable kernel Example
- Functional calculus for a diagonal operator Example
- Integral operator trace under a valid diagonal hypothesis Example
- Legendre polynomials from Gram–Schmidt Example
- Pvm of a diagonal normal operator Example
- The Haar orthonormal basis of L²((0,1)) Example
- The standard basis of ℓ²(ℕ) Example
- Only countably many coefficients of a square-summable family are nonzero Lemma
- Positive square root of a compact positive operator Lemma
- Singular values equal approximation numbers Lemma
- Square-summable orthogonal families have norm-convergent finite sums Lemma
- The finite Bessel inequality and best approximation by a finite orthonormal family Lemma
- The trigonometric characters are orthonormal in L² of the torus Lemma
- Schatten p classes Remark
- A Hilbert space with a dense sequence has a finite or countable orthonormal basis Theorem
- A Hilbert space with a given orthonormal basis is ℓ² of the index set Theorem
- Cyclicity of the trace Theorem
- Existence of a maximal orthonormal family, and maximality as completeness Theorem
- Fourier expansion in a Hilbert space Theorem
- Hilbert Schmidt operators form a two sided ideal Theorem
- Hilbert–Schmidt operators are compact Theorem
- L two kernels give Hilbert–Schmidt operators Theorem
- Min-max principle below the essential spectrum Theorem
- Parseval equivalences for an orthonormal family Theorem
- Singular value decomposition for compact operators Theorem
- Spectral theorem for compact self adjoint operators Theorem
- The Bessel inequality for an arbitrary orthonormal family Theorem
- The Fourier basis and Parseval's identity on the finite torus Theorem
- The Hilbert–Schmidt norm is basis independent Theorem
…and 5 more results.
Dependency tree · two levels
14 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 2.62 and Exercise 2.63, p.87 (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.1, pp.47–48 (standard reference, not scraped)