PhyslibAlpha.ProbabilisticTheory.HilbertSpace.State.Density

Density operators

i. Overview

A positive operator `ρ` with trace `1` defines the state `x ↦ Tr (x ρ)`. The trace here is the linear-algebra trace, so this applies to finite-dimensional Hilbert spaces.

ii. Key results

`UnitalPositiveLinearMap.ofDensity` : the state of a density operator.

2 declarations

definition

State defined by a density operator $\rho$

#ofDensity

Let $H$ be a complex Hilbert space and $\mathcal{L}(H)$ be the space of continuous linear operators on $H$ . Given a positive operator $\rho \in \mathcal{L}(H)$ such that its trace $\text{Tr}(\rho) = 1$ (a density operator), this definition constructs the corresponding state. This state is a unital positive linear map that maps an operator $x \in \mathcal{L}(H)$ to the complex number $\text{Tr}(x \rho)$ .

theorem

The State Defined by Density Operator $\rho$ Maps $x$ to $\text{Tr}(x \rho)$

#ofDensity_apply

Let $H$ be a complex Hilbert space and $\mathcal{L}(H)$ be the space of continuous linear operators on $H$ . For a positive operator $\rho \in \mathcal{L}(H)$ with trace $\text{Tr}(\rho) = 1$ , the state defined by $\rho$ (a unital positive linear map) applied to an operator $x \in \mathcal{L}(H)$ is equal to $\text{Tr}(x \rho)$ .