Physlib

PhyslibAlpha.ProbabilisticTheory.HilbertSpace.TraceClass.RankOne

Rank-one positive operators

i. Overview

The positive rank-one operator `|x⟩⟨x|` is trace class, with trace and trace norm `‖x‖²`. This is the normalization of vector states.

ii. Key results

  • `isTraceClass_rankOne_self` : `|x⟩⟨x|` is trace class.
  • `trace_rankOne_self`, `traceNorm_rankOne_self` : its trace and trace norm are `‖x‖²`.

4 declarations

theorem

Re⁡⟨bi,(∣x⟩⟨x∣)bi⟩=∣⟨x,bi⟩∣2\operatorname{Re} \langle b_i, (|x\rangle\langle x|) b_i \rangle = |\langle x, b_i \rangle|^2 for a Hilbert basis {bi}\{b_i\}

Let HH be a complex Hilbert space and x∈Hx \in H be a vector. For any Hilbert basis {bi}i∈w\{b_i\}_{i \in w} and any index i∈wi \in w, the real part of the diagonal matrix element of the rank-one operator ∣x⟩⟨x∣|x\rangle\langle x| (denoted in the formal statement as `InnerProductSpace.rankOne ℂ x x`) with respect to bib_i satisfies Re⁡⟨bi,(∣x⟩⟨x∣)bi⟩=∣⟨x,bi⟩∣2 \operatorname{Re} \langle b_i, (|x\rangle\langle x|) b_i \rangle = |\langle x, b_i \rangle|^2 where ⟨⋅,⋅⟩\langle \cdot, \cdot \rangle denotes the inner product and ∥⋅∥\|\cdot\| denotes the norm.

theorem

∣x⟩⟨x∣|x\rangle\langle x| is Trace-Class

Let HH be a complex Hilbert space. For any vector x∈Hx \in H, the rank-one operator ∣x⟩⟨x∣|x\rangle\langle x| is trace-class.

theorem

Tr⁡(∣x⟩⟨x∣)=∥x∥2\operatorname{Tr}(|x\rangle\langle x|) = \|x\|^2

Let HH be a complex Hilbert space. For any vector x∈Hx \in H, the trace of the rank-one operator ∣x⟩⟨x∣|x\rangle\langle x| is equal to the square of the norm of xx: Tr⁡(∣x⟩⟨x∣)=∥x∥2\operatorname{Tr}(|x\rangle\langle x|) = \|x\|^2 where Tr⁡\operatorname{Tr} denotes the trace and ∥⋅∥\|\cdot\| denotes the norm in HH.

theorem

Trace Norm of ∣x⟩⟨x∣|x\rangle\langle x| is ∥x∥2\|x\|^2

Let HH be a complex Hilbert space. For any vector x∈Hx \in H, the trace norm of the rank-one operator ∣x⟩⟨x∣|x\rangle\langle x| is equal to the square of the norm of xx, denoted as ∥x∥2\|x\|^2.