Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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 H be a nonzero complex Hilbert space with TB(H) (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). The absolute value of T is the bounded positive operator

T:=(TT)1/2,

the unique bounded positive square root of TT supplied by the positive-square-root theorem (Positive square root).

Well-definedness. TT is self-adjoint and positive: (TT)=TT by the involution rule, and TTx,x=Tx,Tx=Tx20 for every x 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 T is a well-defined bounded positive operator; indeed T0 and T2=TT. Moreover T is self-adjoint: positivity makes Tx,x real for every x, hence (TT)x,x=0, and the four-term polarization identity applied to the sesquilinear form (x,y)(TT)x,y gives T=T.

The two identities used later. For every x,

Tx2=Tx,Tx=TTx,x=T2x,x=TTx,x=Tx2,

so Tx=Tx; consequently Tx=0 exactly when Tx=0, that is kerT=kerT, and T=T because the two operators have the same unit-ball images of norms. The absolute value depends on T through the self-adjoint operator TT, and the square root lies in C(I,TT); 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