The Quantum Formalization Drive

This mission develops Chapter 5 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Quantum Shannon theory repeatedly replaces a mixed state by a pure state on a larger system. A noisy state $\rho_A$ of a system $A$ can always be viewed as the reduced state of a pure state $|\psi\rangle_{RA}$ in which $A$ is entangled with a reference system $R$ that nobody holds. This is the purification viewpoint of Chapter 5 of M. M. Wilde, From Classical to…

Strong subadditivity of the von Neumann entropy is the basic inequality of quantum information theory: most entropy inequalities used in quantum Shannon theory, the data-processing inequality for quantum mutual information, and many capacity converses rest on it (Nielsen–Chuang, ch. 11). This mission formalizes the route to it presented by M. A. Nielsen and…

A quantum circuit may create a state whose full list of amplitudes is far too large for a classical computer to store. That fact alone does not show that every observable feature of its output is hard to estimate. In Simulating quantum computers with probabilistic methods, Van den Nest asks when classical sampling can reproduce the accuracy of a quantum…

A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and $T$ gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore…

We develop a formalism for distilling a classical key from a quantum state in a systematic way, expanding on our previous work on secure key from bound entanglement [K. Horodecki et. al., Phys. Rev. Lett. 94 (2005)]. More detailed proofs, discussion and examples are provided of the main results. Namely, we demonstrate that all quantum cryptographic…

We determine the two-way quantum, entanglement-distribution, private, and secret-key capacities of the pure-loss bosonic channel under an unconditional mean transmitted-photon-number constraint. For transmissivity $η$ and mean photon number $N$, all four capacities coincide and are given by $g(N)-g((1-η)N)$, where $g$ is the entropy of a thermal mode. This resolves…

Quantifying Coherence establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

This mission develops Chapter 6 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.

Shor's algorithm factors an integer $N$ in time polynomial in its binary length, and in doing so threatens the RSA protocol, whose security rests on factoring being hard for classical computers (Shor 1994/1997). Every hardware proposal for running it, including the linear nearest-neighbour architectures studied in A. G. Fowler's thesis Towards Large-Scale…

The quantum capacity of a channel is the largest rate at which it can transmit quantum information reliably. Most capacity formulas of information theory are additive: two channels used side by side are worth the sum of their individual values. Quantum capacity is not. Smith and Yard found two channels, each with zero quantum capacity, whose tensor product…

Mutual information measures how much two attributes of a data set depend on each other. A pair of numbers does not describe three attributes. In the exclusive or, $C=A+B \pmod 2$, each pair is independent while the triple is fully determined. A triplicated attribute, $A=B=C$, is the opposite case: every pair is fully dependent, and given one attribute the other…

The impossibility of perfectly copying (or cloning) an arbitrary quantum state is one of the basic rules governing the physics of quantum systems. The processes that perform the optimal approximate cloning have been found in many cases. These "quantum cloning machines" are important tools for studying a wide variety of tasks, e.g. state estimation and…

A quantum state of two systems can be correlated without being entangled, and the question of which of those unentangled correlations are still "quantum" has been studied from several directions: quantum discord (Ollivier & Zurek 2001), the classical correlations of Henderson & Vedral 2001, and the work-deficit of Oppenheim, Horodecki et al. 2002. Piani,…

A two-qubit gate whose qubits sit in different laboratories cannot be applied by local operations and classical communication (LOCC) alone: it can create entanglement, so it must consume some. The basic question of distributed quantum computation is how much. The textbook answer, teleporting one qubit to the other side, applying the gate and teleporting…

A necessary condition for reversibility (sufficiency) of a quantum channel with respect to complete families of states with bounded rank is obtained. A full description (up to isometrical equivalence) of all quantum channels reversible with respect to orthogonal and nonorthogonal complete families of pure states is given. Some applications in quantum…

Many two-party quantum protocols, such as oblivious transfer and password-based identification, start the same way: Alice sends Bob $n$ qubits $|x\rangle_\theta$ encoding random bits $x$ in random BB84 bases $\theta\in\{+,\times\}^n$. Their security proofs work only against a restricted Bob, for example one with bounded quantum memory (Damgård, Fehr, Salvail,…

The ultimate rates of quantum communication over optical fibre — how many secret bits or entangled pairs per channel use a lossy line can carry with unlimited local operations and classical communication (LOCC) — are bounded through a technique called teleportation stretching (Pirandola, Laurenza, Ottaviani, Banchi, arXiv:1510.08863). The idea is that if a…

The path of a light beam changes when the transparent material through which it travels moves. This matters when interpreting light bending and phase shifts around a flowing liquid, and when asking whether a dielectric can imitate some effects of curved spacetime. Leonhardt and Piwnicki gave a geometrical-optics treatment of a moving, nondispersive…

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives…

Many quantum algorithms end in a measurement that succeeds only with some probability $a$. Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude…

This mission develops Chapter 1 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

This mission develops Chapter 9 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701…

In spectral theory the resolvent of a self-adjoint operator $A$ is studied through scalar functions $F_\psi(z) = \langle \psi, (A - z)^{-1}\psi\rangle$, defined for non-real $z$. Each $F_\psi$ is holomorphic on the upper half plane and maps it into itself. The spectral theorem, in the form presented in G. Teschl's Mathematical Methods in Quantum Mechanics (AMS…