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 A⊆R, 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πi∫ab[(T−(t+iε))−1−(T−(t−iε))−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 z∉R the function gz(λ):=(λ−z)−1 is bounded and Borel on σ(T), with ∥gz∥∞≤∣Im⁡z∣−1, and its Borel calculus value satisfies (T−zI)−1=ΦE(gz): indeed (T−zI)ΦE(gz)=ΦE((λ−z)gz)=ΦE(1)=I and ΦE(gz)(T−zI)=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 Φ(∫Ef dμ)=∫EΦf dμ (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.1A1A2A3

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(gt−iε) is a continuous B(H)-valued function on the compact interval and the Bochner integral converges.

1.2A2algebra

Scalar kernel: for real λ and t one computes (λ−(t+iε))−1−(λ−(t−iε))−1=2iε(λ−t)2+ε2, hence the bounded Borel function Kε(λ):=12πi∫ab[(λ−(t+iε))−1−(λ−(t−iε))−1]dt equals 1π∫abε dt(λ−t)2+ε2=1π[arctan⁡b−λε−arctan⁡a−λε], with ∣Kε∣≤1 and, for every real λ, Kε(λ)→1(a,b)(λ)+121{a,b}(λ) as ε↓0.

2.1step 1.1step 1.2A3

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πi∫ab[(T−(t+iε))−1−(T−(t−iε))−1]dt=12πi∫ab[ΦE(gt+iε)−ΦE(gt−iε)]dt=ΦE(12πi∫ab[gt+iε−gt−iε]dt)=ΦE(Kε).

3.1step 2.1A4

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.

4.1step 3.1A5∎

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)).

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