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.
Orthogonal decomposition by a closed subspace
Statement
Assume the Axiom of Countable Choice. Let be a closed linear subspace of a real or complex Hilbert space . Then every has a unique decomposition
so that as a direct sum of the subspace and its orthogonal complement.
Facts & Assumptions
A linear subspace is convex and contains , and the nearest point of a nonempty closed convex subset of a Hilbert space exists and is unique (Linear subspace of a vector space, Projection onto a nonempty closed convex set).
A point is the nearest point of a closed convex set to exactly when for every (Variational characterisation of the nearest point).
The pairing is linear in the first argument and conjugate-linear in the second, is a linear subspace, and with forces (Orthogonality and the orthogonal complement, Real and complex inner-product spaces and their induced length).
Countable Choice is the selection principle consumed by the nearest-point theorem (The Axiom of Countable Choice ()).
Proof
Given: Countable Choice, a Hilbert space , a closed linear subspace and a vector .
Since is a nonempty closed convex set, has a unique nearest point in .
The variational inequality gives for every . For , take and to obtain . Over the pairing is real-valued, so this already gives . Over , also , and the same real-part conclusion applied to gives . Thus in either scalar field for every , that is .
Setting and gives a decomposition with and .
If are two such decompositions, then lies in , since both and are linear subspaces, so and ; hence , , and the decomposition is unique.
Depends on
Used by
- Orthonormal eigenbasis for a compact self adjoint operator Corollary
- The elliptic kernel and cokernel are finite dimensional Corollary
- The unitary dual need not be Hausdorff Counterexample
- Deficiency subspaces and deficiency indices Definition
- Efficient score and efficient information Definition
- Fredholm determinant of a trace-class operator Definition
- Hilbert-space Moore–Penrose inverse Definition
- Isometry coisometry and partial isometry Definition
- Nondegenerate star-representations of a Banach star-algebra Definition
- Projection valued measure Definition
- The Hardy boundary space, Szegő projection and Szegő kernel on a smoothly bounded domain Definition
- The Hilbert orthogonal projection onto a closed subspace Definition
- Property (T) for finite groups via normalized counting measure Example
- A coercive Hilbert-complex estimate solves the closed equation Lemma
- A residual and a spectral separation bound an invariant-subspace gap Lemma
- Arbitrary-Hilbert Fredholm determinant from a separable reducing support Lemma
- Bounded density and finite-vector transitivity for C*-representations Lemma
- Bounded multipliers on compact self-adjoint eigenspaces define bounded operators Lemma
- Bounded sequences in a separable Hilbert space have weakly convergent subsequences Lemma
- C star state GNS construction, purity and Polish pure-state spaces Lemma
- Closed square-integrable adjoint one-forms on a cusped hyperbolic three-manifold are exact Lemma
- Compact-operator Tikhonov residuals are continuous and increase from range distance to data norm Lemma
- Finite-rank spectral pieces of a self-adjoint compact convolution operator Lemma
- GCR kernel and Mackey Borel characterizations Lemma
- Integrated pressure recovery and MINI pressure-primitive convergence Lemma
- Irreducible representations separate arbitrary C star algebras Lemma
- Kernel projection gives dense conforming gauge approximants Lemma
- Mackey-Shoda irreducibility criterion for monomial representations Lemma
- Maximal orthogonal family of cyclic reducing subspaces Lemma
- Normal relative property (T) controls the distance to the invariant subspace Lemma
- Polar decomposition inside a von Neumann algebra and nonzero partial isometries between nonzero projections in a factor Lemma
- Positive square root of a compact positive operator Lemma
- Second-order L2 approximation by the MINI Fortin map Lemma
- Smooth and K-finite vectors are dense and stable under the derived action Lemma
- Spectral convergence under collectively compact positive approximations Lemma
- The Hilbert-space Babuška–Nečas–Babuška criterion Lemma
- The Matérn native space has its weighted Fourier norm and strict Gram positivity Lemma
- The restricted Matérn native space is the Sobolev quotient space Lemma
- The shifted Hilbert-space normal operator is invertible with inverse norm at most 1/λ Lemma
- Trace decomposition through generalized eigenspaces and the invariant quotient Lemma
…and 33 more results.
Dependency tree · two levels
31 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, Lemma 5.37, p.238 (standard reference, not scraped)
- Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, Theorem 180 (standard reference, not scraped)
- Bruce Blackadar, Ilijas Farah and Asaf Karagila, Hilbert spaces without the Countable Axiom of Choice, Corollary 2.0.5 (standard reference, not scraped)