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.
Polar decomposition for bounded operators
Statement
Assume AC. Every bounded operator on a nonzero complex Hilbert space has a unique partial isometry with and ; its initial space is and its final space is .
Facts & Assumptions
is positive, , and (Absolute value of a bounded operator).
and , so for the closure of the range is (Kernel–range orthogonality for Hilbert adjoints).
For the closed subspace the space decomposes as and the orthogonal projection is the linear self-adjoint idempotent with range and kernel (Orthogonal decomposition by a closed subspace, The Hilbert orthogonal projection onto a closed subspace).
is a partial isometry when it vanishes on and is isometric on , with initial space and final space ; a bounded operator isometric on a closed subspace and zero on its orthogonal complement is a partial isometry (Isometry coisometry and partial isometry, Partial isometry characterizations).
A bounded linear map that is isometric on a subspace extends uniquely to an isometry on its closure, since the Hilbert space is complete and the extension is obtained by limits of Cauchy images; the operator norm controls such extensions (Hilbert space, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).
AC is the hypothesis of the square-root and Hilbert-space suppliers (The Axiom of Choice).
Proof
Given: A nonzero complex Hilbert space and a bounded operator , with and .
The subspace is closed with , and .
The assignment on is well defined, because implies and hence , and it is isometric, because .
extends uniquely to a bounded linear isometry on the closure of its domain: an isometry on a dense subspace is uniformly continuous, its images of Cauchy sequences are Cauchy and converge by completeness, and the limit is independent of the sequence.
Extend to by on ; then is bounded and linear, , and is isometric on , so is a partial isometry with initial space and final space .
: for every one has and by construction.
Uniqueness: if is a partial isometry with and , then on the dense subspace of one has ; both and vanish on and both are continuous, so and agree on and on , hence .
Therefore is the unique partial isometry with and , with initial space and final space , as asserted.
Depends on
- Absolute value of a bounded operator
- Partial isometry characterizations
- Orthogonal decomposition by a closed subspace
- The Axiom of Choice
- Kernel–range orthogonality for Hilbert adjoints
- Isometry coisometry and partial isometry
- The Hilbert orthogonal projection onto a closed subspace
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum
- Hilbert space
Used by
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
- John B. Conway, A Course in Functional Analysis, 2nd ed., Polar Decomposition 3.11, printed pp.239–243 (standard reference, not scraped)
- Theo Bühler and Dietmar Salamon, Functional Analysis, §5.3, printed pp.235–245 (standard reference, not scraped)