Physlib

PhyslibAlpha.AlgebraicFramework.WStarAlgebra.RankOnePairing

Rank-one tests for the concrete predual pairing

Ported from `unbounded-alpha-public`'s `WStarAlgebra/RankOnePairing.lean`. The surjectivity proof needs rank-one operators as test observables. This module exposes the corresponding formula with an arbitrary trace-class second argument; it is the matrix-coefficient identity used to recover positivity of a predual representative of a normal state.

2 declarations

theorem

Trace of rank-one operator Tr(∣x⟩⟨y∣)=⟨y,x⟩\text{Tr}(|x\rangle\langle y|) = \langle y, x \rangle

Let HH be a complex Hilbert space. For any vectors x,y∈Hx, y \in H, the trace of the rank-one operator ∣x⟩⟨y∣|x\rangle\langle y| (the operator defined by z↦⟨y,z⟩xz \mapsto \langle y, z \rangle x) is equal to the inner product of yy and xx: Tr(∣x⟩⟨y∣)=⟨y,x⟩\text{Tr}(|x\rangle\langle y|) = \langle y, x \rangle

theorem

Tr(∣x⟩⟨y∣T)=⟨y,Tx⟩\text{Tr}(|x\rangle\langle y| T) = \langle y, Tx \rangle

Let HH be a complex Hilbert space. For any trace-class operator T∈S1(H)T \in \mathcal{S}_1(H) and any vectors x,y∈Hx, y \in H, the trace pairing of the rank-one operator ∣x⟩⟨y∣|x\rangle\langle y| with TT is equal to the inner product of yy and TxTx: Tr((∣x⟩⟨y∣)T)=⟨y,Tx⟩\text{Tr}((|x\rangle\langle y|) T) = \langle y, Tx \rangle where ∣x⟩⟨y∣|x\rangle\langle y| is the rank-one operator defined by the map z↦⟨y,z⟩xz \mapsto \langle y, z \rangle x.