We survey progress in understanding quantum information in terms of equivalences, reducibilities, and asymptotically achievable rates for transformations among nonlocal resources such as classical communication, entanglement, and particular quantum states or channels. In some areas, eg source coding, there are straightforward parallels to classical information theory; in others eg entanglement-assisted communication, new effects and tradeoffs appear that are beginning to be fairly well understood, or the remaining uncertainty has become focussed on a few simple open questions, such as conjectured additivity of the Holevo capacity. In still other areas, e.g. the role of the back communication and the classification of tripartite entanglement, much remains unknown, and it appears unlikely that an adequate description exists in terms of a finite number of resources.
We survey progress in understanding quantum information in terms of equivalences, reducibilities, and asymptotically achievable rates for transformations among nonlocal resources such as classical communication, entanglement, and particular quantum states or channels. In some areas, eg source coding, there are straightforward parallels to classical information theory; in others eg entanglement-assisted communication, new effects and tradeoffs appear that are beginning to be fairly well understood, or the remaining uncertainty has become focussed on a few simple open questions, such as conjectured additivity of the Holevo capacity. In still other areas, e.g. the role of the back communication and the classification of tripartite entanglement, much remains unknown, and it appears unlikely that an adequate description exists in terms of a finite number of resources.
We survey progress in understanding quantum information in terms of equivalences, reducibilities, and asymptotically achievable rates for transformations among nonlocal resources such as classical communication, entanglement, and particular quantum states or channels. In some areas, eg source coding, there are straightforward parallels to classical information theory; in others eg entanglement-assisted communication, new effects and tradeoffs appear that are beginning to be fairly well understood, or the remaining uncertainty has become focussed on a few simple open questions, such as conjectured additivity of the Holevo capacity. In still other areas, e.g. the role of the back communication and the classification of tripartite entanglement, much remains unknown, and it appears unlikely that an adequate description exists in terms of a finite number of resources.
Information and computation theory have undergone a spurt of new growth, and a renewal of their historic connection to basic physics, as they have expanded to treat the intact transmission and processing of quantum states, and the interaction of such 'quantum information' with traditional forms of information. We may wonder why this did not happen earlier, as quantum principles have long been accepted as fundamental to all of physics. Perhaps the founders of information and computation theory, such as Shannon, Turing and von Neumann, were too accustomed to thinking of information processing in macroscopic terms, not yet having before them the powerful examples of the genetic code and ever-shrinking microelectronics. Be that as it may, information until recently has largely been thought of in classical terms, with quantum mechanics playing a supporting role in the design of the equipment to process it, and setting limits on the rate at which it could be sent through certain channels. Now we know that a fully quantum theory of information and information processing offers, among other benefits, a brand of cryptography whose security rests on fundamental physics, and a reasonable hope of constructing quan- tum computers that could dramatically speed up the solution of certain mathematical problems. These benefits depend on distinc- tively quantum properties such as uncertainty, interference and entanglement. At a more fundamental level, it has become clear that an information theory based on quantum principles extends and completes classical information theory, just as complex numbers extend and complete the reals. Besides quantum generalizations of classical notions such as sources, channels and codes, the new theory includes two complementary, quantifiable kinds of information— classical information and quantum entanglement. Classical infor- mation can be copied at will, but can only be transmitted forward in time, to a receiver in the sender's forward light cone. Entanglement in contrast, cannot be copied, but can connect any two points in space-time. Conventional data processing operations destroy entanglement, but quantum operations can create it and use it for various purposes, such as speeding up certain classical computa- tions and assisting in the transmission of classical information or intact quantum states. Part of the new quantum information theory is the qualitative and quantitative study of entanglement, and its interactions with classical information. Any means, such as an optical fibre, of delivering quantum systems more or less intact from one place to another, may be viewed as a quantum channel. Unlike classical channels, which are well characterized by a single capacity, quantum channels have several distinct capacities, depending on what one is trying to use them for, and what auxiliary resources are brought into play. New effects involving quantum information continue to be discovered, not only in the traditional areas of computation, channel capacity, and cryptography, but in areas such as commu- nication complexity and game theory.
Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean 4 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.
Abstract This book has discussed the foundations of quantum information science as well as the relationship between physics and information theory in general. It has considered the quantum equivalents of the Shannon coding and channel capacity theorems. The von Neumann entropy plays a role analogous to the Shannon entropy, and the Holevo bound is the analogue of Shannon's mutual information used to quantify the capacity of a classical channel. Quantum systems can process information more efficiently than classical systems in a number of different ways. Quantum teleportation and quantum dense coding can be performed using quantum entanglement. Entanglement is an excess of correlations that can exist in quantum physics and is impossible to reproduce classically (with what is termed “separable” states). The book has also demonstrated how to discriminate entangled from separable states using entanglement witnesses, as well as how to quantify entanglement, and looked at quantum computation and quantum algorithms.
Abstract This book deals with the basic concept of information, its importance, and the similarities and differences between classical and quantum information. First, classical information theory and its application to communication are discussed. Quantum mechanics and communication based on the laws of quantum mechanics are then considered. Quantum entanglement, a key resource in quantum communication, is analysed both from the fundamental perspective and from the perspective of its information-processing capability. This book also introduces quantum computation (in the context of the search and factorisation algorithms) and the basics of quantum error correction. Throughout this book, the connections between information theory, thermodynamics, and (quantum) physics are emphasised and discussed. Other topics covered in the book are data compression, related measures of information such as relative entropy, joint entropy, conditional entropy, and mutual information, along with the capacity of a noisy channel.