PhyslibAlpha.ProbabilisticTheory.WStarAlgebra.RankOnePairing

Rank-one operators in the trace pairing

i. Overview

For a bounded operator `A` and a trace-class operator `T`, the trace pairing of `A |x⟩⟨y|` with `T` is a matrix coefficient. This recovers a predual element from its values on rank-one operators.

ii. Key results

`trace_rankOne_formula` : the trace of a rank-one operator times a trace-class operator.
`TraceClass.tracePairing_rankOne_left` : the trace pairing with a rank-one operator.

2 declarations

theorem

$\operatorname{Tr}(|x\rangle\langle y|) = \langle y, x \rangle$

#trace_rankOne_formula

Let $H$ be a complex Hilbert space. For any vectors $x, y \in H$ , the trace of the rank-one operator $|x\rangle\langle y|$ (the operator defined by $v \mapsto \langle y, v \rangle x$ ) is equal to the inner product $\langle y, x \rangle_{\mathbb{C}}$ .

theorem

$\text{tracePairing}(|x\rangle\langle y|, T) = \langle y, Tx \rangle$

#tracePairing_rankOne_left

Let $H$ be a complex Hilbert space. For any trace-class operator $T$ on $H$ and vectors $x, y \in H$ , the trace pairing of the rank-one operator $|x\rangle\langle y|$ (defined by the mapping $v \mapsto \langle y, v \rangle x$ ) with $T$ is given by the inner product of $y$ and $Tx$ : $\text{tracePairing}(|x\rangle\langle y|, T) = \langle y, Tx \rangle$