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.
Absolute value of a bounded operator
Definition
Assume AC and let be a nonzero complex Hilbert space with (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). The absolute value of is the bounded positive operator
the unique bounded positive square root of supplied by the positive-square-root theorem (Positive square root).
Well-definedness. is self-adjoint and positive: by the involution rule, and for every by the adjoint identity (Hilbert-adjoint identities, Self-adjoint, positive, unitary and normal operators). The square root theorem therefore applies and its root is unique, so is a well-defined bounded positive operator; indeed and . Moreover is self-adjoint: positivity makes real for every , hence , and the four-term polarization identity applied to the sesquilinear form gives .
The two identities used later. For every ,
so ; consequently exactly when , that is , and because the two operators have the same unit-ball images of norms. The absolute value depends on through the self-adjoint operator , and the square root lies in ; no polar decomposition or Borel calculus is used in its definition.
Depends on
Used by
Dependency tree · two levels
25 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., Chapter IX §3, 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)