Alphabeta Math
TheoremStatement: AI-adaptedProof: 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.

Stone resolvent formula for spectral projections

Statement

Assume AC. Let T be a bounded self-adjoint operator on a nonzero complex Hilbert space H with spectral projection valued measure E on the compact set σ(T)R, and let a<b be real. For every Borel set AR, write E(A):=E(Aσ(T)). Then, with the resolvents (T(t±iε))1 defined for ε>0 by Spectrum and resolvent of a bounded operator and the integral of a continuous B(H)-valued function understood in the Bochner sense (Bochner-integrable function),

12πiab[(T(t+iε))1(T(tiε))1]dt  E((a,b))+E({a})+E({b})2

in the strong operator topology as ε0. In particular, if a,bσ(T) then the limit is the spectral projection E((a,b)), and the half-masses at a and b appear exactly when these points are atoms of the spectrum.

Facts & Assumptions

[A1]

For zR the function gz(λ):=(λz)1 is bounded and Borel on σ(T), with gzImz1, and its Borel calculus value satisfies (TzI)1=ΦE(gz): indeed (TzI)ΦE(gz)=ΦE((λz)gz)=ΦE(1)=I and ΦE(gz)(TzI)=I by linearity and multiplicativity of the Borel calculus (Borel functional calculus for bounded normal operators, Borel functional calculus for a bounded normal operator).

[A2]

σ(T)R for self-adjoint T, so the functions gz are defined on the spectrum (Spectrum of a self adjoint operator is real).

[A3]

A continuous function on the compact interval [a,b] with values in the Banach space B(H) is Bochner integrable, and a bounded linear map Φ satisfies Φ(Efdμ)=EΦfdμ (Bochner integrability criterion, Bounded linear maps commute with Bochner integration).

[A4]

The Borel calculus is a unital star-homomorphism: ΦE(1B)=E(B), and uniformly bounded pointwise E-almost everywhere convergence implies strong convergence (Pvm integral is a star homomorphism, Projection valued measure).

[A5]

AC is the declared choice hypothesis of this page from the construction item onward (The Axiom of Choice).

Proof

technique · direct

Given: A bounded self-adjoint operator T with spectral PVM E on σ(T)R, real numbers a<b, and ε>0.

1.1

Resolvent identity: since σ(T)R, the function gz is bounded Borel for z=t±iε and (A1) identifies (T(t±iε))1=ΦE(gt±iε), so the integrand tΦE(gt+iε)ΦE(gtiε) is a continuous B(H)-valued function on the compact interval and the Bochner integral converges.

A1A2A3
1.2

Scalar kernel: for real λ and t one computes (λ(t+iε))1(λ(tiε))1=2iε(λt)2+ε2, hence the bounded Borel function Kε(λ):=12πiab[(λ(t+iε))1(λ(tiε))1]dt equals 1πabεdt(λt)2+ε2=1π[arctanbλεarctanaλε], with Kε1 and, for every real λ, Kε(λ)1(a,b)(λ)+121{a,b}(λ) as ε0.

A2algebra
2.1

The operator integral is the calculus value of the kernel: by linearity of ΦE and commutation of the bounded linear map ΦE with Bochner integration, 12πiab[(T(t+iε))1(T(tiε))1]dt=12πiab[ΦE(gt+iε)ΦE(gtiε)]dt=ΦE(12πiab[gt+iεgtiε]dt)=ΦE(Kε).

step 1.1step 1.2A3
3.1

Strong limit: Kε1 and Kε1(a,b)+121{a,b} pointwise, so the strong-convergence clause of the calculus gives ΦE(Kε)ΦE(1(a,b)+121{a,b})=E((a,b))+12(E({a})+E({b})) in the strong operator topology.

step 2.1A4
4.1

Therefore the resolvent expression converges strongly to E((a,b))+12(E({a})+E({b})) as ε0; if a,bσ(T) the endpoint atoms vanish and the limit is the open-interval spectral projection E((a,b)).

step 3.1A5

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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