- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
A linear map \(E : M_{D}(\mathbb {C}) \to M_{D}(\mathbb {C})\) is completely positive (CP) if it admits a Kraus representation: there exist operators \(\{ K_i\} _{i=0}^{r-1}\) with \(K_i \in M_{D}(\mathbb {C})\) such that, for every \(X \in M_{D}(\mathbb {C})\),
The Kraus representation also gives entrywise positivity on every positive block matrix by Theorem 2.2.1, and hence the associated completely positive map between matrix \(C^*\)-algebras in Theorem 2.2.2.
A Fitting decomposition of a linear endomorphism \(f:V\to V\) on a finite-dimensional vector space over an algebraically closed field consists of:
\(f\) is nilpotent on the generalized \(0\)-eigenspace,
\(f\) is invertible on each generalized \(\mu \)-eigenspace for \(\mu \neq 0\),
the generalized eigenspaces span \(V\),
the generalized eigenspaces are linearly independent.
A linear map \(E : M_{D}(\mathbb {C}) \to M_{D}(\mathbb {C})\) is irreducible if whenever \(P\) is an orthogonal projection satisfying \(E(P M_{D}(\mathbb {C}) P) \subseteq P M_{D}(\mathbb {C}) P\), then \(P = 0\) or \(P = \mathbb {1}\). This is [ Wol12 , Theorem 6.2(1) ] . The definition applies to any linear map; complete positivity is not required.
Let \(K=\{ K^i\} _{i=0}^{d-1}\) be a finite family of \(D\times D\) matrices. For a word \(w=(i_1,\ldots ,i_n)\), its word evaluation is
with the empty word evaluated as the identity matrix.
Given operators \(\{ K_i\} _{i=0}^{d-1}\) with \(K_i \in M_{D}(\mathbb {C})\), the Kraus map is
A linear map is completely positive (Definition 2.1.5) if and only if it can be written in this form, as in (1).
The fixed-length vector span at length \(n\) is
This is \(S_n(K)|\varphi \rangle \) in the notation of [ SPGWC10 ] .
If \(C\in M_{D}(\mathbb {C})\) is nonzero, then
This is the matrix-factorization input used in [ PGVWC07 , Lemma 3 ] .
Let \(T_N(K)\) be the span of the products of at most \(N\) matrices from a finite family \(K\). If \(D{\gt}0\) and \(T_N(K)=M_{D}(\mathbb {C})\), then there are a word \(w\), a nonzero scalar \(\mu \), and a nonzero vector \(\varphi \in \mathbb {C}^D\) such that
Let \(K=(K^i)_{i=0}^{d-1}\) be a finite family of \(D\times D\) matrices, where \(D{\gt}0\), and suppose that \(S_n(K)=M_{D}(\mathbb {C})\) for every sufficiently large \(n\). If \(\varphi \neq 0\), \(\mu \neq 0\), and \(K^{i_0}\varphi =\mu \varphi \), then \(H_{D-1}(K,\varphi )=\mathbb {C}^D\).
Suppose \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \). If \(p{\gt}0\) and \(\rho ,\sigma \) are nonzero positive-semidefinite fixed points of \(\mathcal{E}_K^p\), then \(\sigma =c\rho \) for some \(c\in \mathbb {C}\).
Let \(K=\{ K^i\} _{i=0}^{d-1}\) be a finite family of \(D\times D\) matrices, where \(D{\gt}0\), and let \(\varphi \neq 0\). If, for some \(N\), words in \(K\) of length at most \(N\) span \(M_{D}(\mathbb {C})\), then the vectors \(K^w\varphi \) with \(|w|\leq D-1\) span \(\mathbb {C}^D\).
For every choice of \(d\), \(D\), and \(K\) as above and every \(q\ge 0\), suppose \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \). Then every nonzero positive-semidefinite fixed point of \(\mathcal{E}_K\) is positive definite.
Let \(K\) be a finite matrix family with Kraus map \(E\), and let \(Q\) be an orthogonal projection. If
for every \(X\in M_{D}(\mathbb {C})\), then \((\mathbb {1}-Q)K_iQ=0\) for every \(i\).
For every choice of \(d\), \(D\), and \(K\) as above, every \(q\ge 0\), and every \(\varphi \in \mathbb {C}^D\),
Let \(I\) be finite, let \((K_i)_{i\in I}\) be a family in \(M_{D}(\mathbb {C})\), and set \(E(X)=\sum _i K_iXK_i^\dagger \). For every non-negative integer \(N\),
For \(N=0\), the product is the identity matrix.
Let \(D{\gt}0\), and let \(K=\{ K^i\} _{i=0}^{d-1}\) be a finite family of \(D\times D\) matrices satisfying
Suppose there is a common length \(q\ge 0\) such that \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \in \mathbb {C}^D\). Then there is a positive-definite matrix \(\rho \) such that \(\mathcal{E}_K(\rho )=\rho \).
For every choice of \(d\), \(D\), and \(K\) as above and every \(q\ge 0\), suppose \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \). Then \(\mathcal{E}_K^q(\rho ){\gt}0\) for every nonzero positive-semidefinite matrix \(\rho \).
For every choice of \(d\), \(D\), and \(K\) as above and every \(q\ge 0\), suppose \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \). For every \(p{\gt}0\), each nonzero positive-semidefinite fixed point of \(\mathcal{E}_K^p\) is positive definite.
Let \(D{\gt}0\), and let \(K=\{ K^i\} _{i=0}^{d-1}\) be a finite family of \(D\times D\) matrices satisfying
Suppose there is a common length \(q\ge 0\) such that \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \in \mathbb {C}^D\). Then the Kraus map \(\mathcal{E}_K\) is primitive: it has a nonzero fixed point and \(1\) is its only peripheral eigenvalue.
For every choice of \(d\), \(D\), and \(K\) as above and every \(q\ge 0\), suppose \(H_q(K,\varphi )=\mathbb {C}^D\) for every nonzero \(\varphi \in \mathbb {C}^D\). Then \(\mathcal{E}_K^q(|\varphi \rangle \! \langle \varphi |){\gt}0\) for every \(\varphi \neq 0\).
Let \(E\colon M_{D}(\mathbb {C})\to M_{D}(\mathbb {C})\) be linear, and let \(\rho \) and \(\sigma \) be positive-definite fixed points of \(E\). Suppose every nonzero positive-semidefinite fixed point of \(E\) is positive definite. Then \(\sigma =c\rho \) for some \(c\in \mathbb {C}\).
Let \(E\colon M_D(\mathbb C)\to M_D(\mathbb C)\) be a positive, trace-preserving linear map and \(X=E(X)\) a fixed point. Decompose \(X\) into Hermitian and anti-Hermitian parts and then each into orthogonal positive and negative parts, yielding four positive semidefinite operators \(P_1,\dots ,P_4\). Then \(E(P_j)=P_j\) for \(j=1,\dots ,4\); in other words, every fixed point is a \(\mathbb C\)-linear combination of four positive-semidefinite fixed points. In particular, if \(E\) is a channel and \(H=H^\dagger \) is fixed by \(E\), then there are positive-semidefinite fixed points \(Q_1,Q_2\) such that \(H=Q_1-Q_2\).
This is Wolf Proposition 6.8.