Dependencies

A set of Kraus operators \(\{ K_i\} _{i=1}^r \subset M_q(\mathbb {C})\) defines a quantum channel (or a trace-preserving map) if they satisfy the completeness relation:

where \(I_q\) is the \(q \times q\) identity matrix.

A set of Kraus operators \(\{ K_i\} _{i=1}^r \subset M_q(\mathbb {C})\) defines a quantum operation if they satisfy:

In this context, \(\le \) denotes the Loewner order, meaning \(I_q - \sum K_i^\dagger K_i\) is a positive semi-definite matrix.

A matrix \(\rho \in M_q(\mathbb {C})\) is a density matrix (or a normalized state) if it satisfies:

1. \(\rho \ge 0\) (Positive semi-definite)

2. \(\operatorname {Tr}(\rho ) = 1\) (Normalization)

A matrix \(\rho \in M_q(\mathbb {C})\) is a sub-normalized density matrix if it satisfies:

1. \(\rho \ge 0\) (Positive semi-definite)

2. \(\operatorname {Tr}(\rho ) \le 1\)

These often represent states after a non-deterministic measurement.

Let \(\Phi : M_q(\mathbb {C}) \to M_q(\mathbb {C})\) be a map defined by a set of Kraus operators \(\{ K_i\} _{i=1}^r\) satisfying the quantum channel condition \(\sum _i K_i^\dagger K_i = I_q\). Then for any \(\rho \in M_q(\mathbb {C})\), the trace is preserved:

Let \(\Phi \) be a quantum channel defined by Kraus operators \(\{ K_i\} \) such that \(\sum _i K_i^\dagger K_i = I\). If \(\rho \) is a normalized matrix with \(\operatorname {Tr}(\rho ) = 1\), then the output of the channel is also normalized:

Let \(\mathcal{D}_q\) denote the set of \(q \times q\) density matrices (positive semi-definite matrices with unit trace). A quantum channel \(\Phi \) induces a well-defined map:

mapping \(\rho \mapsto \sum _i K_i \rho K_i^\dagger \). This map is well-defined because it preserves both the positive semi-definite property and the unit trace of the input state.

Let \(\Sigma \) be an alphabet and \(\mathcal{K} : \Sigma \to (\text{Fin } r \to M_q(R))\) be a function mapping each symbol to a Kraus family. For a word \(w\) of length \(n\), the iterated application map \(\delta ^* : (\text{Fin } n \to \Sigma ) \to M_q(R) \to M_q(R)\) is defined recursively by:

where \(\Phi _{a}(\sigma ) = \sum _{i \in \text{Fin } r} K_{a,i} \sigma K_{a,i}^\dagger \) is the completely positive map associated with the symbol \(a \in \Sigma \), and \(\text{init}(w)\) denotes the prefix of the word of length \(n-1\).

Let \(\Sigma \) be an alphabet where each symbol \(a \in \Sigma \) is associated with a quantum channel \(\Phi _a\) (satisfying \(\sum _i K_{a,i}^\dagger K_{a,i} = I\)). For any word \(w \in \Sigma ^n\) and any initial density matrix \(\rho \), the state after processing the word, \(\rho _w = \delta ^*(w, \rho )\), satisfies:

1. \(\rho _w \ge 0\) (Positive Semi-definiteness)

2. \(\operatorname {Tr}(\rho _w) = 1\) (Trace Preservation)

In other words, \(\delta ^*(w, \cdot )\) is a well-defined map from \(\mathcal{D}_q\) to \(\mathcal{D}_q\).

Let \(\rho \in M_k(\mathbb {C})\) be a density matrix (\(\rho \ge 0\) and \(\operatorname {Tr}(\rho ) = 1\)). Let \(\{ \mathbf{e}_i\} _{i=1}^k\) be the standard basis vectors in \(\mathbb {C}^k\), where \(\mathbf{e}_i\) has a 1 at index \(i\) and 0 elsewhere. The pure state projection associated with outcome \(i\) is defined as:

The resulting probability mass function (PMF) over the set of outcomes \(\{ 1, \dots , k\} \) is defined by the assignment:

Let \(\rho \in M_{mn}(\mathbb {C})\) be a density matrix on a composite system \(\mathcal{H}_A \otimes \mathcal{H}_B\). The partial trace over the right subsystem (\(\mathcal{H}_B\)) is the map \(\text{Tr}_B : M_{mn}(\mathbb {C}) \to M_m(\mathbb {C})\) defined by the components:

Given a Kraus family \(\{ K_i\} _{i=1}^r \subset M_m(\mathbb {C})\), the Stinespring operator \(V \in M_{mr \times m}(\mathbb {C})\) is defined as:

where \(\mathbf{e}_i\) are the standard basis vectors of the environment space \(\mathbb {C}^r\).

The Stinespring dilation of a state \(\rho \) relative to the operator \(V\) is the matrix in the enlarged space:

It follows that the original Kraus map is recovered by \(\Phi (\rho ) = \text{Tr}_B(V \rho V^\dagger )\).

Let \(\{ K_i\} _{i=1}^r \subset M_m(\mathbb {C})\) be a family of Kraus operators and \(\rho \in M_m(\mathbb {C})\) be a density matrix. Let \(V = \sum _{i} K_i \otimes \mathbf{e}_i\) be the Stinespring operator. Then:

where \(\operatorname {Tr}_B\) denotes the partial trace over the environment space \(\mathbb {C}^r\).

Let \(\{ K_i\} _{i=1}^r \subset M_m(\mathbb {C})\) be a family of operators satisfying the trace-non-increasing (TNI) condition \(\sum _i K_i^\dagger K_i \le I\). The orthogonal CPTP completion is the operator \(V_{comp} \in M_{m(r+1) \times m}(\mathbb {C})\) defined block-wise as:

In Lean notation, this is represented by branching on the index \(x.2\): using the Stinespring operator for the first \(r\) indices and the deficit root \(\Delta \) for the last index.

If the initial operators satisfy \(\sum _i K_i^\dagger K_i \le I\), then the completion \(V_{comp}\) is an isometry, i.e.,

A basis state density matrix has trace one.

An automaton based on a quantum channel maps density matrices to density matrices while reading a single letter.

Let \(R\) be a star-ring with an additive commutative monoid structure. Given a family of matrices \(\{ K_i\} _{i=1}^r \in M_q(R)\), the Kraus application map \(\Phi : M_q(R) \to M_q(R)\) is defined as the completely positive map:

where \(K_i^\dagger \) denotes the conjugate transpose of the \(i\)-th Kraus operator \(K_i\).

Kraus operators preserve the PSD property.

Transition function \(\delta ^*\) corresponding to a word over an alphabet, where each symbol is mapped to a completely positive map in Kraus form, of rank at most \(r\).

An automaton based on a quantum channel maps density matrices to density matrices while reading a word.

Let \(\mathcal{A} = (\Sigma , \mathcal{K}, \rho _0, P_{\text{acc}})\) be a Measure-Once Quantum Finite Automaton. The language accepted by \(\mathcal{A}\) with cutpoint \(\lambda = \frac{1}{2}\) is the set of words:

where:

• \(\delta ^*(w, \rho _0)\) is the state after processing word \(w\).

• \(P_{\text{acc}} = \mathbf{e}_{\text{acc}} \mathbf{e}_{\text{acc}}^\top \) is the projection onto the accepting state.

• The index \(1\) in the probability mass function represents the “Accept” outcome.

A probability mass function on two orthogonal projections \(P, P^{\bot }\), with measure equal to the trace of the density matrix \(\rho \) times the projection.

Let \(\rho \in M_q(R)\) be a positive semi-definite matrix (\(\rho \ge 0\)). Then for any Kraus operators \(\{ K_i\} \), the result of the map

is also positive semi-definite.

A pure state is PSD.

Projection-valued measure.

A projection-valued measure, with measure equal to the trace of the density matrix \(\rho \) times the projection.

Let \(\rho \in M_k(\mathbb {R})\) be a density matrix, and let \(\text{acc} \in \{ 1, \dots , k\} \) be the designated acceptance index. The probability distribution over the outcomes \(\{ 0, 1\} \) (Reject, Accept) is given by the PMF:

where \(P_{\text{acc}} = \mathbf{e}_{\text{acc}} \mathbf{e}_{\text{acc}}^\top \) is the projection onto the accepting basis state.

Quantum channel.

If \(P\) is a projection and \(\rho \) is PSD then the trace of \(P\rho \) is nonnegative.

If \(A\) and \(B\) are PSD then \(AB\) has nonnegative trace.