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 tR. 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 limt01t(U(t)xx) exists exactly for xD(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)x2=h2dEx, h(T)=h(T), and h1(T)h2(T)=(h1h2)(T); the truncation definition gives g(T)x=limmgm(T)x for xDg (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 xD(T) one has (Ta)x2=(λ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.1

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)x2=eitλ2dEx=dEx=x2 and U(t)=U(t)=U(t)1.

A1
1.2

Strong continuity: for xH and tt0, U(t)xU(t0)x2=eitλeit0λ2dEx0 by [A3], the integrand being bounded by 4 and tending to 0 pointwise.

A1A3
1.3

Derivative at 0 for xD(T): 1t(U(t)xx)iTx2=1t(eitλ1)iλ2dEx0 by [A3], since 1t(eitλ1)iλ2λ and λ2 is Ex-integrable exactly because xD(T) by [A2].

A2A3
2.1

Converse: if z=limn1tn(U(tn)xx) for some sequence tn0, then by [A2] and Fatou's lemma λ2dExlim infn1tn(eitnλ1)2dEx=lim infn1tn(U(tn)xx)2=z2<, so xD(T); step 1.3 then identifies the full limit as iTx.

A2A3step 1.3
3.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].

A2A4step 1.1step 1.2step 2.1

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