QuantumInfo.Finite.Channel.DegradableOrder

The Degradable Order

We define the "degradable order" on channels, where M ≤ N if N can be degraded to M. This is a scoped instance, because there are other reasonable orders on channels.

The degradable order is actually only a preorder, because channels that are degradable to each other are not necessarily equal. (For instance, unitary channels are degradable to the identity and vice versa.) It can compare channels of different output dimensions, but they must have the same input dimension. For this reason the `DegradablePreorder` is parameterized by the channel input type.

One might hope that if this was defined on the quotient type of "channels up to unitary equivalence" that it would become an order; but this is not the case. That is, there are channels `A → B` that are degradable to each other, but cannot be degraded to each other by unitary operations. For instance, let A be the replacement channel that goes to a mixed state, and B be a replacement channel that goes to a pure state.

Technical notes: to model "channels of different output types", the preorder is on the Sigma type of channels parameterized by their output type. And since the output type needs to be a Fintype and DecidableEq, the argument is also a Sigma to bring this along.

1 declaration

definition

The degradable preorder on quantum channels $\Lambda_1 \le \Lambda_2 \iff \Lambda_2$ is degradable to $\Lambda_1$

#DegradablePreorder

For a fixed input space $\mathcal{H}_{in}$ (indexed by the finite type $dIn$ ), the degradable preorder is a preorder defined on the set of all quantum channels (CPTP maps) $\Lambda: \mathcal{L}(\mathcal{H}_{in}) \to \mathcal{L}(\mathcal{H}_{out})$ where the output space $\mathcal{H}_{out}$ can vary. Specifically, the carrier set consists of pairs $(dOut, \Lambda)$ , where $dOut$ specifies the output dimension and its required structures (finite type and decidable equality), and $\Lambda$ is a CPTP map from $dIn$ to $dOut$ . A channel $\Lambda_1$ is said to be less than or equal to $\Lambda_2$ ( $\Lambda_1 \le \Lambda_2$ ) if $\Lambda_2$ is degradable to $\Lambda_1$ . That is, $\Lambda_1 \le \Lambda_2$ if there exists a CPTP map $D: \mathcal{L}(\mathcal{H}_{out_2}) \to \mathcal{L}(\mathcal{H}_{out_1})$ such that $\Lambda_1 = D \circ \Lambda_2$ .

QuantumInfo.Finite.Channel.DegradableOrder

The Degradable Order

The degradable preorder on quantum channels Λ1≤Λ2 ⟺ Λ2\Lambda_1 \le \Lambda_2 \iff \Lambda_2Λ1​≤Λ2​⟺Λ2​ is degradable to Λ1\Lambda_1Λ1​

The degradable preorder on quantum channels $\Lambda_1 \le \Lambda_2 \iff \Lambda_2$ is degradable to $\Lambda_1$