Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

A self-adjoint operator generates a strongly continuous unitary group

Statement

Assume the Axiom of Choice. Let T be a self-adjoint operator on H with spectral projection valued measure E, and set U(t):=eitT=∫Reitλ dE(λ) for t∈R. Then U is a strongly continuous one-parameter unitary group, U(t)D(T)=D(T) and TU(t)=U(t)T on D(T), and the derivative lim⁡t→01t(U(t)x−x) exists exactly for x∈D(T), where it equals iTx. Thus the generator of U is G=iT, with D(G)=D(T).

Facts & Assumptions

[A1]

For bounded Borel h the operator h(T) is bounded with ∥h(T)x∥2=∫∣h∣2dEx, h(T)∗=h‾(T), and h1(T)h2(T)=(h1h2)(T); the truncation definition gives g(T)x=lim⁡mgm(T)x for x∈Dg (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).

[A2]

D(T)={x:∫λ2dEx<∞}, and for x∈D(T) one has ∥(T−a)x∥2=∫(λ−a)2dEx for real a; also U(t)D(T)=D(T) and TU(t)=U(t)T on D(T), since U(t)=eitλ(T) commutes with E(B) and products of functions multiply (Spectral theorem for unbounded self-adjoint operators (PVM form), Unbounded Borel functional calculus: domains, products, spectral mapping).

[A3]

Scalar dominated convergence and Fatou's lemma apply to the finite measures Ex (Dominated convergence, Fatou's lemma).

[A4]

The generator is defined by the difference quotients of the statement, and D(G) is a linear subspace (Infinitesimal generator of a unitary group).

Proof

technique · direct

Given: A self-adjoint T with spectral PVM E, and U(t)=eitT.

1.1A1

Unit and group law: U(t) is bounded, U(t)U(s)=(eitλeisλ)(T)=U(t+s) and U(0)=I by [A1], and U(t) is unitary because ∥U(t)x∥2=∫∣eitλ∣2dEx=∫dEx=∥x∥2 and U(t)∗=U(−t)=U(t)−1.

1.2A1A3

Strong continuity: for x∈H and t→t0, ∥U(t)x−U(t0)x∥2=∫∣eitλ−eit0λ∣2dEx→0 by [A3], the integrand being bounded by 4 and tending to 0 pointwise.

1.3A2A3

Derivative at 0 for x∈D(T): ∥1t(U(t)x−x)−iTx∥2=∫∣1t(eitλ−1)−iλ∣2dEx→0 by [A3], since ∣1t(eitλ−1)−iλ∣≤2∣λ∣ and ∣λ∣2 is Ex-integrable exactly because x∈D(T) by [A2].

2.1A2A3step 1.3

Converse: if z=lim⁡n1tn(U(tn)x−x) for some sequence tn→0, then by [A2] and Fatou's lemma ∫λ2dEx≤lim inf⁡n∫∣1tn(eitnλ−1)∣2dEx=lim inf⁡n∥1tn(U(tn)x−x)∥2=∥z∥2<∞, so x∈D(T); step 1.3 then identifies the full limit as iTx.

3.1A2A4step 1.1step 1.2step 2.1∎

By steps 1.1, 1.2, 1.3 and 2.1 the family U is a strongly continuous one-parameter unitary group whose generator satisfies D(G)=D(T) and G=iT; the invariance and commutativity claims for U(t) on D(T) are [A2].

Depends on

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