Email Gateway (Jul 07 2025 at 10:04): Email Gateway (Jul 07 2025 at 10:04):From: Tobias Nipkow <nipkow@in.tum.de>
Kraus Maps
Dominique Unruh
We formalize Kraus maps, i.e., quantum channels of the form ... for suitable
families of ``Kraus operators''. (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 of families of Kraus operators (Kraus families for short), from
trace-class operators on Hilbert space to those on , indexed by of type . This
induces both a Kraus map, as well as a quantum measurement with outcomes of type
.... 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 ... for some Kraus family, and restate our results in terms of such
functions.
https://www.isa-afp.org/entries/Kraus_Maps.html
Enjoy!
Last updated: Jul 26 2025 at 12:43 UTC