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.
Order on bounded self adjoint operators
Definition
Assume Countable Choice and let be a nonzero complex Hilbert space. Write
for the set of bounded self-adjoint operators on (Self-adjoint, positive, unitary and normal operators). For define
Equivalently ; the notation is exactly the positivity of Self-adjoint, positive, unitary and normal operators. Operators are compared only when both are self-adjoint: the relation is not defined for a general pair in , and no conjugate-linear or non-real quadratic form is admitted by the definition.
is a real vector space and is a partial order on it. Sums and real scalar multiples of self-adjoint operators are self-adjoint, because the adjoint is conjugate-linear and (Hilbert-adjoint identities); the zero operator is self-adjoint. So the comparisons below are between elements of a real vector space.
- Reflexivity. and , so .
- Transitivity. If and , then for every by additivity of the pairing in its first argument, so .
- Antisymmetry. If and , then for every . The sesquilinear form is linear in and conjugate-linear in and satisfies for every , so the four-term expansion vanishes for all . Hence for all , and fixing and taking gives , so and . The expansion is the displayed consequence of additivity and conjugate-linearity alone, so antisymmetry consumes no completeness of (Hilbert space).
Two conventions. First, the order is a partial order on the real vector space of self-adjoint operators; it is not a total order, and the extrema of the spectrum in the later results are taken in , not by comparing operators. Second, refers to the quadratic form of a self-adjoint operator; the counterexample on the companion page shows that nonnegativity of the spectrum alone does not define positivity for operators that are not self-adjoint (The operator norm as the least bound and as the unit-sphere or unit-ball supremum for the operator data used throughout).
Depends on
Used by
- Self adjointness cannot be dropped from the order calculus Counterexample
- Sign and positive negative parts of a self adjoint operator Example
- Square root and absolute value of a matrix Example
- Positive square root and covariance matrices Remark
- Positive square root Theorem
- Self adjoint norm and spectrum extrema Theorem
Dependency tree · two levels
20 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, §5.4, printed pp.245–255 (standard reference, not scraped)
- Dana P. Williams, Lecture Notes on the Spectral Theorem, §4, pp.10–13 (standard reference, not scraped)