### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Quantum computing
- Mathematics/Physics/Quantum information

### Session Projective_Measurements

- Linear_Algebra_Complements
- Projective_Measurements
- CHSH_Inequality

### Depends on

- Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
- Quantum Hoare Logic

### Used by

- Simultaneous diagonalization of pairwise commuting Hermitian matrices

## Cite

×

Projective_Measurements-AFP

    @article{Projective_Measurements-AFP,
      author  = {Mnacho Echenim},
      title   = {Quantum projective measurements and the CHSH inequality},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Projective_Measurements.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Mar 9, 2021 : Isabelle2021