Quantum projective measurements and the CHSH inequality in Isabelle/HOL
Logic in Computer Science
2021-03-16 v1
Abstract
We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.
Keywords
Cite
@article{arxiv.2103.08535,
title = {Quantum projective measurements and the CHSH inequality in Isabelle/HOL},
author = {Mnacho Echenim and Mehdi Mhalla},
journal= {arXiv preprint arXiv:2103.08535},
year = {2021}
}