Abstract
We formalize Kraus maps, i.e., quantum channels of the form
$\rho\mapsto\sum_x M_x\rho M_x^\dagger$ for suitable families of
``Kraus operators'' $M_x$. (In the finite-dimensional setting and the
setting of separable Hilbert spaces, those are known to be equivalent
to completely-positive maps, another common formalization of quantum
channels.) Our results hold for arbitrary (i.e., not necessarily
finite-dimensional or separable Hilbert spaces.
Specifically, in theory Kraus_Families, we formalize the type
$(\alpha,\beta,\xi)\ \mathtt{kraus\_family}$ of families of Kraus
operators $M_x$ (Kraus families for short), from trace-class operators
on Hilbert space $\alpha$ to those on $\beta$, indexed by $x$ of type
$\xi$. This induces both a Kraus map $\rho\mapsto\sum_x M_x\rho
M_x^\dagger$, as well as a quantum measurement with outcomes of type
$\xi$.
We define and study various special Kraus families such as zero,
identity, application of an operator, sum of two Kraus maps,
sequential composition, infinite sum, random sampling, trace, tensor
products, and complete measurements.
Furthermore, since working with explicit Kraus families can be
cumbersome when the specific family of operators is not relevant, in
theory Kraus_Maps, we define a Kraus map to be a function between two
spaces that is of the form $\rho\mapsto\sum_x M_x\rho M_x^\dagger$ for
some Kraus family, and restate our results in terms of such functions.