The Quantum Formalization Drive

We study and solve the problem of distilling secret key from quantum states representing correlation between two parties (Alice and Bob) and an eavesdropper (Eve) via one-way public discussion: we prove a coding theorem to achieve the "wire-tapper" bound, the difference of the mutual information Alice-Bob and that of Alice-Eve, for so-called…

We characterize the bath resources needed to supply repeated uses of a fixed finite-dimensional quantum channel in a closed device. For each horizon $T$, one bath, one initial state and one repeated unitary are fixed before the user. Each output is returned before the next input arrives; no reset, discard, fresh ancilla or uncounted controller is available.…

In this paper we fill the gap in previous works by proving the formula for entanglement-assisted capacity of quantum channel with additive constraint (such as bosonic Gaussian channel). The main tools are the coding theorem for classical-quantum constrained channels and a finite dimensional approximation of the input density operators for…

The Schur transform, which block-diagonalizes the tensor representation $U^{\otimes n}$ of the unitary group $\mathbf{U}_d$ on $n$ qudits, is an important primitive in quantum information and theoretical physics. We give a generalization of its quantum circuit implementation due to Bacon, Chuang, and Harrow (SODA 2007) to the case of mixed tensor …

The maximum rates for reliably transmitting classical information over Bosonic multiple-access channels (MACs) are derived when the transmitters are restricted to coherent-state encodings. Inner and outer bounds for the ultimate capacity region of the Bosonic MAC are also presented. It is shown that the sum-rate upper bound is achievable with a…

In this paper we study the subset of generalized quantum measurements on finite dimensional systems known as local operations and classical communication (LOCC). While LOCC emerges as the natural class of operations in many important quantum information tasks, its mathematical structure is complex and difficult to characterize. Here we provide a precise…

In view of controlling finite dimensional open quantum systems, we provide a unified Lie-semigroup framework describing the structure of completely positive trace-preserving maps. It allows (i) to identify the Kossakowski-Lindblad generators as the Lie wedge of a subsemigroup, (ii) to link properties of Lie semigroups such as divisibility with Markov…

The classical capacity of a noisy optical channel is the maximum rate at which information can be transmitted reliably, given a constraint on the mean input energy. For the ubiquitous bosonic Gaussian channels, which include standard models of loss and noise in fibre and free-space optical links, determining this rate requires addressing whether…

We give a representation for entanglement-breaking channels in separable Hilbert space that generalizes the "Kraus decomposition with rank one operators" and use it to describe the complementary channels. We also give necessary and sufficient condition of entanglement-breaking for a general quantum Gaussian channel. Application of this condition to one-mode…

The work is devoted to study of quantum mutual information and coherent information -- the two important characteristics of quantum communication channel. Appropriate definitions of these quantities in the infinite-dimensional case are given and their properties are studied in detail. Basic identities relating quantum mutual information and coherent…

We analyse two possible definitions of the squashed entanglement in an infinite-dimensional bipartite system: direct translation of the finite-dimensional definition and its universal extension. It is shown that the both definitions produce the same lower semicontinuous entanglement measure possessing all basis properties of the squashed entanglement on the…

A classification of one-mode Gaussian channels is given up to canonical unitary equivalence. A complementary to the quantum channel with additive classical Gaussian noise is described providing an example of one-mode Gaussian channel which is neither degradable nor anti-degradable.

In this paper we give a general integral representation for separable states in the tensor product of infinite dimensional Hilbert spaces and provide the first example of separable states that are not countably decomposable. We also prove the structure theorem for the quantum communication channels that are entanglement-breaking, generalizing the…

We give trade-offs between classical communication, quantum communication, and entanglement for processing information in the Shannon-theoretic setting. We first prove a unit-resource capacity theorem that applies to the scenario where only the above three noiseless resources are available for consumption or generation. The optimal strategy mixes the three…

A provable quantum advantage for approximate optimization via decoded quantum interferometry establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

An Optimal Quantum Linear Systems Algorithm establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Sample-optimal learning of stabilizer states establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Efficient Exact Quantum Sampling from the Sun-Wootters Distribution for Optimal Polynomial Intersection establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Worst-Case Quantum Algorithm for Optimal Polynomial Intersection Beyond Decoded Quantum Interferometry establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Hamiltonian Decoded Quantum Interferometry for General Pauli Hamiltonians establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Multivariate Decoded Quantum Interferometry for Weighted Optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Randomized and quantum approximate matrix multiplication establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Fast Convex Optimization with Quantum Gradient Methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Quantum Signal Processing and Quantum Singular Value Transformation on $U(N)$ establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Quantum speedups for stochastic optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.