Quantum version of Markov’s inequality
Given events E1,…Et with probability p1,…,pt, the union bound states that the probability that neither event Ei occurs is at least 1-(p1+…pt). Markov’s inequality gives more refined information: it states that, for any a>0, the probability that more than a(p1+…+pt) events Ei occur is at most 1/a.
The union bound has a very elegant generalization to quantum information. Here, events are specified by projections and their probability is related to their dimension. But there is no known analogue of Markov’s inequality! The goal of this project is to determine if such an analogue can hold. To start, the student will read the formulation of all the known inequalities and guess a possible form for a quantum Markov. The student may then perform numerical simulations to test the validity of their conjecture. Ideally, a proof of the conjecture can be obtained via linear algebra.
Level:
This is approachable at the Bachelors or Masters level
Background:
Solid knowledge of finite dimensional linear algebra. Introduction to quantum information or computation course.
Contact:
[email protected]
Formalizing quantum non-locality proofs in lean
Lean is a proof verification tool popular in the mathematics community. It is currently less used in computer science and quantum information. The goal of this project is to develop the foundations of non-local games in lean. For example, a possible concrete goal would be to write a lean proof of Tsirelson’s inequality, which bounds quantum success in the CHSH inequality. Longer term, the goal is to develop enough foundations in quantum information and in complexity theory to derive a complete lean proof of the result MIP*=RE (https://arxiv.org/abs/2001.04383).
Level:
This is a Masters level project
Background:
A course in quantum information or computation, and a course in formal verification.
Contact:
[email protected]