Quantum projective measurements and the CHSH inequality

Abstract

This work contains a formalization of quantum projective measurements, also known as von Neumann measurements, which are based on elements of spectral theory. We also formalized the CHSH inequality, an inequality involving expectations in a probability space that is violated by quantum measurements, thus proving that quantum mechanics cannot be modeled with an underlying local hidden-variable theory.

Publication
Archive of Formal Proofs

Formal proof development in Isabelle, supplement to [Echenim2021]