LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Support of the spectral measure, the spectrum and the values of the scalar law

Statement

Assume the Axiom of Choice and the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a nonzero complex Hilbert space (Hilbert space) and let $A$ be a self-adjoint operator on $H$ with spectral projection-valued measure $E_{A}$ on the Borel $σ$ -algebra of $R$ and spectrum $σ (A)$ (Spectral theorem for unbounded self-adjoint operators (PVM form), Resolvent and spectrum of an unbounded operator). Then:

(a) $E_{A} (R ∖ σ (A)) = 0$ , equivalently $E_{A} (B) = E_{A} (B \cap σ (A))$ for every Borel set $B \subseteq R$ ; and $E_{A} (U) \neq 0$ for every nonempty relatively open subset $U \subseteq σ (A)$ . Thus the support of $E_{A}$ is exactly $σ (A)$ .

(b) For every density operator $ρ$ on $H$ , the scalar law $μ_{ρ}^{A} (B) = tr (ρ E_{A} (B))$ of Density operators and scalar spectral probability clause (b) satisfies $μ_{ρ}^{A} (B) = μ_{ρ}^{A} (B \cap σ (A)) and μ_{ρ}^{A} (σ (A)) = 1$ for every Borel set $B$ : no mass lies outside the spectrum.

(c) More generally, if $C \subseteq R$ is a Borel set with $E_{A} (C) = 0$ , then $μ_{ρ}^{A} (C) = 0$ for every density operator $ρ$ , and if $E_{A} (C) = E_{A} (R)$ then $μ_{ρ}^{A} (C) = 1$ .

Facts & Assumptions

Given: The Axiom of Choice and the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )); a nonzero complex Hilbert space $H$ ; a self-adjoint operator $A$ with spectral PVM $E_{A}$ and spectrum $σ (A)$ ; density operators $ρ$ on $H$ .

[F1]

Spectrum from the calculus. The spectrum of $f (A)$ is the essential range ${z \in C : E_{A} (f^{- 1} (B_{ε} (z))) \neq 0 for every ε > 0}$ of the Borel function $f$ with respect to $E_{A}$ , and for $f (λ) = λ$ the operator $f (A)$ is $A$ with domain $D (A)$ ; consequently, for real $z$ , $z \in σ (A)$ if and only if $E_{A} ((z - ε, z + ε)) \neq 0$ for every $ε > 0$ (Unbounded Borel functional calculus: domains, products, spectral mapping, Spectral theorem for unbounded self-adjoint operators (PVM form)).

[F2]

Projection-valued measure. $E_{A}$ takes values in orthogonal projections, $E_{A} (\emptyset) = 0$ , $E_{A} (R) = I$ , $E_{A} (B \cap C) = E_{A} (B) E_{A} (C)$ , and for pairwise disjoint Borel $B_{n}$ with union $B$ the series $\sum_{n} E_{A} (B_{n}) x$ converges in norm to $E_{A} (B) x$ for every $x$ (Projection valued measure).

[F3]

Monotonicity and vanishing. If $B \subseteq C$ then $E_{A} (B) = E_{A} (B) E_{A} (C) = E_{A} (C) E_{A} (B)$ and $E_{A} (C) - E_{A} (B) = E_{A} (C ∖ B)$ is an orthogonal projection with range orthogonal to the range of $E_{A} (B)$ ; hence $⟨ E_{A} (B) x, x ⟩ \leq ⟨ E_{A} (C) x, x ⟩$ for every $x$ . Consequently, if $E_{A} (C) = 0$ then $E_{A} (B) = 0$ for every Borel $B \subseteq C$ (Projection valued measure, Scalar and complex measures from a pvm).

[F4]

Scalar law. For a density operator $ρ$ and a PVM $E$ the assignment $B \mapsto tr (ρ E (B))$ is a probability measure with $tr (ρ E (B)) = \sum_{n} w_{n} ∥ E (B) u_{n} ∥^{2}$ in every expansion $ρ = \sum_{n} w_{n} T_{u_{n}, u_{n}}$ , $w_{n} \geq 0$ , $\sum_{n} w_{n} = 1$ , $(u_{n})$ orthonormal; in particular $E (B) = 0$ implies $tr (ρ E (B)) = 0$ and $E (B) = I$ implies $tr (ρ E (B)) = 1$ (Density operators and scalar spectral probability clauses (a) and (b)).

[F5]

Countable dense subset. The set $Q$ is countable and dense in $R$ ( $Q$ is countably infinite, Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

Proof

1.1givenF1F2algebra

[The spectrum is the essential range of the identity] By [F1] applied to $f (λ) = λ$ , $σ (A)$ is the essential range of the identity with respect to $E_{A}$ . For real $z$ this says: $z \in σ (A)$ if and only if $E_{A} ((z - ε, z + ε)) \neq 0$ for every $ε > 0$ ; and for non-real $z$ , taking $0 < ε < ∣ Im z ∣$ gives $B_{ε} (z) \cap R = \emptyset$ , where $B_{ε} (z) : = {w \in C : ∣ w - z ∣ < ε}$ , so $E_{A} (B_{ε} (z) \cap R) = E_{A} (\emptyset) = 0$ by [F2] and no non-real point lies in the essential range.

2.1givenstep 1.1F2F3F5algebra

[The open null set equals the complement of the spectrum] Let $I$ be the set of pairs of rationals $p < q$ , countable by [F5], and put $V : = ⋃ {(p, q) : (p, q) \in I, E_{A} ((p, q)) = 0}$ , a countable union of Borel sets. To see $V \subseteq R ∖ σ (A)$ , suppose $z \in V \cap σ (A)$ ; then $z \in (p, q)$ with $E_{A} ((p, q)) = 0$ for some rationals $p < q$ , and choosing $ε > 0$ with $(z - ε, z + ε) \subseteq (p, q)$ gives $E_{A} ((z - ε, z + ε)) = 0$ by [F3], contradicting $z \in σ (A)$ by step 1.1. Conversely, if $z \notin σ (A)$ , step 1.1 supplies $ε > 0$ with $E_{A} ((z - ε, z + ε)) = 0$ , and by density of the rationals [F5] there are rationals $p < z < q$ with $[p, q] \subseteq (z - ε, z + ε)$ ; then $E_{A} ((p, q)) = 0$ by [F3], so $z \in V$ . Hence $V = R ∖ σ (A)$ .

3.1givenstep 2.1F2F3algebra

[The complement of the spectrum is null] The representation of step 2.1 writes $V = R ∖ σ (A)$ as a countable union of Borel null sets. Enumerate these sets as $(I_{n})$ , repeating $\emptyset$ if there are only finitely many, and put $C_{0} : = I_{0}$ and $C_{n} : = I_{n} ∖ ⋃_{k < n} I_{k}$ for $n \geq 1$ . The $C_{n}$ are pairwise disjoint, have union $V$ , and satisfy $E_{A} (C_{n}) = 0$ by monotonicity [F3]. Strong countable additivity [F2] therefore gives $E_{A} (V) x = \sum_{n} E_{A} (C_{n}) x = 0$ for every $x$ , so $E_{A} (V) = 0$ . By additivity [F2], this is equivalent to $E_{A} (B) = E_{A} (B \cap σ (A)) + E_{A} (B ∖ σ (A)) = E_{A} (B \cap σ (A))$ for every Borel $B$ .

4.1step 1.1step 3.1F2F3algebra

[Nonempty relatively open subsets of the spectrum are not null] Let $U \subseteq σ (A)$ be nonempty and relatively open, so $U = σ (A) \cap W$ for some open $W \subseteq R$ . Choose $z \in U$ and $ε > 0$ with $(z - ε, z + ε) \subseteq W$ . By step 1.1, $E_{A} ((z - ε, z + ε)) \neq 0$ because $z \in σ (A)$ ; by step 3.1 applied to the Borel set $(z - ε, z + ε)$ , $E_{A} ((z - ε, z + ε)) = E_{A} ((z - ε, z + ε) \cap σ (A))$ , and $(z - ε, z + ε) \cap σ (A) \subseteq U$ by the choice of $ε$ . Were $E_{A} (U) = 0$ , monotonicity [F3] would give $E_{A} ((z - ε, z + ε) \cap σ (A)) = 0$ , a contradiction; hence $E_{A} (U) \neq 0$ . This proves clause (a) together with step 3.1.

4.2step 3.1F4algebra

[Clause (b)] By step 3.1 and additivity of $E_{A}$ , $E_{A} (B) = E_{A} (B \cap σ (A))$ for every Borel $B$ ; applying the scalar law [F4] to both sides gives $μ_{ρ}^{A} (B) = tr (ρ E_{A} (B)) = tr (ρ E_{A} (B \cap σ (A))) = μ_{ρ}^{A} (B \cap σ (A))$ , and with $B = R$ this reads $μ_{ρ}^{A} (σ (A)) = tr (ρ E_{A} (R)) = tr ρ = 1$ by [F4].

5.1givenF4algebra∎

[Clause (c)] If $E_{A} (C) = 0$ then $tr (ρ E_{A} (C)) = 0$ by [F4] for every density operator; if $E_{A} (C) = I$ then $tr (ρ E_{A} (C)) = tr ρ = 1$ by [F4]. Both statements are instances of the scalar law, and clause (b) is the case $C = B ∖ σ (A)$ and $C = σ (A)$ respectively.

Support of the spectral measure, the spectrum and the values of the scalar law

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources