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.

Affinity and trace-norm continuity of the scalar spectral law

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and let $H$ be a nonzero complex Hilbert space (Hilbert space). Let $A$ be a self-adjoint operator on $H$ with spectral projection-valued measure $E_{A}$ (Projection valued measure). For a self-adjoint trace-class operator $T$ on $H$ (Trace class operator, Trace of a trace class operator) and a Borel set $B \subseteq R$ put $Φ_{T} (B) : = tr (T E_{A} (B)) \in C .$ Then:

(a) $∣ Φ_{T} (B) ∣ \leq ∥ T ∥_{1}$ for every Borel set $B$ ; the map $T \mapsto Φ_{T} (B)$ is real-linear on the self-adjoint trace-class operators; and for every density operator $ρ$ one has $0 \leq Φ_{ρ} (B) \leq 1$ , so that $μ_{ρ}^{A} : = Φ_{ρ}$ is a probability measure on the Borel sets with $μ_{ρ}^{A} (R) = 1$ (Density operators and scalar spectral probability clause (b)).

(b) If $ρ = \sum_{n} w_{n} ρ_{n}$ is a statistical mixture of density operators $ρ_{n}$ with weights $w_{n} \geq 0$ , $\sum_{n} w_{n} = 1$ , the trace-norm convergent sum of The state space is convex, closed under countable mixtures, and complete in the trace norm, then for every Borel set $B$ $μ_{ρ}^{A} (B) = \sum_{n} w_{n} μ_{ρ_{n}}^{A} (B),$ the series converging absolutely.

(c) For density operators $ρ, σ$ one has $\sup {∣ μ_{ρ}^{A} (B) - μ_{σ}^{A} (B) ∣ : B \subseteq R Borel} \leq ∥ ρ - σ ∥_{1},$ and if density operators $ρ_{k}$ converge to $ρ$ in trace norm, then $μ_{ρ_{k}}^{A} (B) \to μ_{ρ}^{A} (B)$ uniformly over all Borel sets $B$ .

Facts & Assumptions

Given: The Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )); a nonzero complex Hilbert space $H$ ; a self-adjoint operator $A$ with spectral PVM $E_{A}$ ; self-adjoint trace-class operators $T$ and density operators $ρ, ρ_{n}, σ$ on $H$ ; Borel sets $B \subseteq R$ .

[F1]

Projections and the trace ideal. Every $E_{A} (B)$ is an orthogonal projection, hence $∥ E_{A} (B) ∥ \leq 1$ ; for trace-class $T$ and bounded $S$ the product $T S$ is trace class with $∥ T S ∥_{1} \leq ∥ T ∥_{1} ∥ S ∥$ (Projection valued measure, Trace class is a two sided Banach operator ideal clause 2).

[F2]

Trace linearity and bound. The trace is linear on the trace-class operators and $∣ tr S ∣ \leq ∥ S ∥_{1}$ for every trace-class $S$ (Trace is absolutely convergent and basis independent clauses 1 and 4).

[F3]

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

[F4]

Convex combinations of states. If $ρ_{n}$ are density operators and $w_{n} \geq 0$ , $\sum_{n} w_{n} = 1$ over a finite or countable index set, then $ρ : = \sum_{n} w_{n} ρ_{n}$ converges in trace norm to a density operator (The state space is convex, closed under countable mixtures, and complete in the trace norm).

Proof

1.1givenF1F2algebra

[Contraction and trace bound] By [F1] the operator $T E_{A} (B)$ is trace class with $∥ T E_{A} (B) ∥_{1} \leq ∥ T ∥_{1} ∥ E_{A} (B) ∥ \leq ∥ T ∥_{1}$ , since $E_{A} (B)$ is an orthogonal projection of norm at most one; [F2] gives $∣ Φ_{T} (B) ∣ = ∣ tr (T E_{A} (B)) ∣ \leq ∥ T E_{A} (B) ∥_{1} \leq ∥ T ∥_{1}$ .

1.2givenF1F2F3algebra

[Real-linearity and positivity on states] For self-adjoint trace-class $S, T$ and real $a, b$ the operator $a S + b T$ is self-adjoint and trace class, and [F2] gives $Φ_{a S + b T} (B) = tr ((a S + b T) E_{A} (B)) = a tr (S E_{A} (B)) + b tr (T E_{A} (B)) = a Φ_{S} (B) + b Φ_{T} (B)$ ; this proves real-linearity. If $ρ$ is a density operator with expansion $ρ = \sum_{n} w_{n} T_{u_{n}, u_{n}}$ , then [F3] gives $Φ_{ρ} (B) = \sum_{n} w_{n} ∥ E_{A} (B) u_{n} ∥^{2} \geq 0$ and $Φ_{ρ} (B) \leq \sum_{n} w_{n} ∥ u_{n} ∥^{2} = 1$ ; together with [F3] this makes $μ_{ρ}^{A} = Φ_{ρ}$ a probability measure.

2.1givenstep 1.2F1F2F4algebra

[Affinity under mixtures] Let $ρ_{n}$ be density operators and $w_{n} \geq 0$ , $\sum_{n} w_{n} = 1$ , with trace-norm convergent sum $ρ = \sum_{n} w_{n} ρ_{n}$ , a density operator by [F4]. Writing $S_{N} : = \sum_{n \leq N} w_{n} ρ_{n}$ , [F1] gives $∥ S_{N} E_{A} (B) - ρ E_{A} (B) ∥_{1} \leq ∥ S_{N} - ρ ∥_{1} ∥ E_{A} (B) ∥ \leq ∥ S_{N} - ρ ∥_{1} \to 0$ ; by [F2] and continuity of the scalar limit, $tr (ρ E_{A} (B)) = \lim_{N} tr (S_{N} E_{A} (B)) = \lim_{N} \sum_{n \leq N} w_{n} tr (ρ_{n} E_{A} (B)) = \sum_{n} w_{n} μ_{ρ_{n}}^{A} (B)$ , the series converging absolutely because the finite partial sums of the nonnegative terms are bounded by the limit $μ_{ρ}^{A} (B) \leq 1$ .

2.2givenstep 1.1algebra

[Uniform trace-norm continuity] For Borel $B$ , $ρ - σ$ is self-adjoint and trace class, so step 1.1 gives $∣ μ_{ρ}^{A} (B) - μ_{σ}^{A} (B) ∣ = ∣ Φ_{ρ - σ} (B) ∣ \leq ∥ ρ - σ ∥_{1}$ ; taking the supremum over Borel sets yields the displayed bound, and the convergence assertion follows by applying it to $ρ_{k} - ρ$ .

3.1step 1.1step 1.2step 2.1step 2.2∎

[Conclusion] Step 1.2 proves the bound, real-linearity, positivity and probability-measure clauses of (a); step 2.1 proves the mixture identity (b); step 2.2 proves the uniform bound and continuity (c).

Affinity and trace-norm continuity of the scalar spectral law

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources