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.
Position operator on L^2(R)
Example
Assume the Axiom of Choice. On let be the multiplication operator by the coordinate function , with domain . Then is self-adjoint with , its spectral PVM is , and defines a strongly continuous unitary group whose generator is ; in particular is a proper dense subspace of .
Facts & Assumptions
On a -finite measure space , for a real measurable multiplier that is finite almost everywhere, the multiplication-operator example gives the domain, self-adjointness, spectral PVM , functional calculus and essential-range spectrum formula on (Multiplication operators: domain, spectral measure and spectrum).
A self-adjoint operator generates the strongly continuous unitary group computed by the Borel calculus, with generator and derivative domain (A self-adjoint operator generates a strongly continuous unitary group, Strongly continuous one-parameter unitary group).
Verification
Given: and the multiplication operator by .
is the multiplication operator of the previous example for the measure space and : the domain, the self-adjointness, the spectral PVM and the calculus are those results.
The essential range of is , since every interval has positive Lebesgue measure, so .
By the generation theorem applied to the self-adjoint operator , the formula is a strongly continuous unitary group with generator , and the calculus of [A1] identifies .
is proper and dense: it is dense by the previous example, and the function for , extended by on , lies in but not in , because diverges.
The claims are steps 1.1, 1.2, 1.3 and 1.4. ∎
Depends on
- Multiplication operators: domain, spectral measure and spectrum
- Spectral theorem for unbounded self-adjoint operators (PVM form)
- Unbounded Borel functional calculus: domains, products, spectral mapping
- A self-adjoint operator generates a strongly continuous unitary group
- Strongly continuous one-parameter unitary group
- The Axiom of Choice
- The space $L^p(\mu)$ as the quotient by null functions
Used by
Dependency tree · two levels
43 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)