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.
A self-adjoint operator generates a strongly continuous unitary group
Statement
Assume the Axiom of Choice. Let be a self-adjoint operator on with spectral projection valued measure , and set for . Then is a strongly continuous one-parameter unitary group, and on , and the derivative exists exactly for , where it equals . Thus the generator of is , with .
Facts & Assumptions
For bounded Borel the operator is bounded with , , and ; the truncation definition gives for (Unbounded Borel functional calculus: domains, products, spectral mapping, The unbounded PVM integral is densely defined, closed and normal, Integral of a measurable function against a projection-valued measure).
, and for one has for real ; also and on , since commutes with and products of functions multiply (Spectral theorem for unbounded self-adjoint operators (PVM form), Unbounded Borel functional calculus: domains, products, spectral mapping).
Scalar dominated convergence and Fatou's lemma apply to the finite measures (Dominated convergence, Fatou's lemma).
The generator is defined by the difference quotients of the statement, and is a linear subspace (Infinitesimal generator of a unitary group).
Proof
Given: A self-adjoint with spectral PVM , and .
Unit and group law: is bounded, and by [A1], and is unitary because and .
Strong continuity: for and , by [A3], the integrand being bounded by and tending to pointwise.
Derivative at for : by [A3], since and is -integrable exactly because by [A2].
Converse: if for some sequence , then by [A2] and Fatou's lemma , so ; step 1.3 then identifies the full limit as .
By steps 1.1, 1.2, 1.3 and 2.1 the family is a strongly continuous one-parameter unitary group whose generator satisfies and ; the invariance and commutativity claims for on are [A2].
Depends on
- Unbounded Borel functional calculus: domains, products, spectral mapping
- Spectral theorem for unbounded self-adjoint operators (PVM form)
- Integral of a measurable function against a projection-valued measure
- Infinitesimal generator of a unitary group
- Dominated convergence
- Fatou's lemma
- The unbounded PVM integral is densely defined, closed and normal
- Symmetric, self-adjoint and essentially self-adjoint operators
- The Axiom of Choice
Used by
Dependency tree · two levels
47 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)