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.
Stone's theorem: unitary groups and self-adjoint generators
Statement
Assume the Axiom of Choice. The map , computed by the Borel functional calculus of (Unbounded Borel functional calculus: domains, products, spectral mapping), is a bijection from the set of self-adjoint operators on onto the set of strongly continuous one-parameter unitary groups on . Its inverse assigns to its generator and the self-adjoint operator ; here is exactly the set of vectors at which is differentiable at , and for .
Facts & Assumptions
For every self-adjoint , is a strongly continuous one-parameter unitary group with generator and (A self-adjoint operator generates a strongly continuous unitary group).
The generator of a strongly continuous unitary group is densely defined and skew-adjoint, so is self-adjoint with (The generator of a unitary group is closed and skew-adjoint, Infinitesimal generator of a unitary group).
If then , , and is differentiable with derivative (Laplace resolvents of a unitary group, Infinitesimal generator of a unitary group).
A skew-symmetric operator satisfies for , because . The generator in [A2] is skew-adjoint and hence skew-symmetric. The generator of a unitary group is closed and skew-adjoint Hilbert space
Proof
Given: A self-adjoint , and a strongly continuous unitary group with generator .
Applying [A1] to produces a strongly continuous unitary group with generator , so the map is well defined, and its derivative at exists exactly on where it equals .
Applying [A2] to produces the self-adjoint operator with ; applying [A1] to gives the strongly continuous unitary group , whose generator is .
Uniqueness for a fixed generator: if are strongly continuous unitary groups with the same generator and , then is differentiable with by [A3], so by [A4], and gives on ; since is dense by [A2] and are isometries, for every .
Hence in step 1.2, that is for the self-adjoint ; combined with step 1.1 this makes a bijection with the stated inverse.
The derivative characterisation is the one from [A1] applied to the self-adjoint : the limit exists exactly on and equals .
Depends on
- The generator of a unitary group is closed and skew-adjoint
- A self-adjoint operator generates a strongly continuous unitary group
- Infinitesimal generator of a unitary group
- Strongly continuous one-parameter unitary group
- Symmetric, self-adjoint and essentially self-adjoint operators
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Hilbert space
- Laplace resolvents of a unitary group
- Unbounded Borel functional calculus: domains, products, spectral mapping
Used by
Dependency tree · two levels
58 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
- Gerald Teschl, Mathematical Methods in Quantum Mechanics, second edition (standard reference, not scraped)
- Dana P. Williams, Lecture Notes on the Spectral Theorem (standard reference, not scraped)
- Roland Schnaubelt, Evolution Equations (lecture notes) (standard reference, not scraped)