Quantum projective measurements and the CHSH inequality. Echenim, M. Archive of Formal Proofs, March, 2021.
Quantum projective measurements and the CHSH inequality [link]Paper  abstract   bibtex   
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.
@article{Echenim2021a,
  title     = {Quantum projective measurements and the CHSH inequality},
  author    = {Echenim, Mnacho},
  year      = {2021},
  month     = mar,
  journal   = {Archive of Formal Proofs},
  volume    = {2021},
  url       = {https://isa-afp.org/entries/Projective_Measurements.html},
  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.},
  webnote   = {Formal proof development in Isabelle, supplement to \cite{Echenim2021}},
  bibsource = qplbib
}

Downloads: 0