### Abstract

The CHSH inequality, named after Clauser, Horne, Shimony and Holt, was used by Alain Aspect to prove experimentally that Einstein's hypothesis stating that quantum mechanics could be defined using local hidden variables was incorrect. The CHSH inequality is based on a setting in which an experiment consisting of two separate parties performing joint measurements is run several times, and a score is derived from these runs. If the local hidden variable hypothesis had been correct, this score would have been bounded by $2$, but a suitable choice of observables in a quantum setting permits to violate this inequality when measuring the Bell state; this is the result that Aspect obtained experimentally. Tsirelson answered the question of how large this violation could be by proving that in the quantum setting, the highest score that can be obtained when running this experiment is $2\sqrt{2}$. Along with elementary results on density matrices which represent quantum states in the finite dimensional setting, we formalize Tsirelson's result and summarize the main results on the CHSH score:

1. Under the local hidden variable hypothesis, this score admits 2 as an upper-bound.
2. When the density matrix under consideration is separable, the upper-bound cannot be violated.
3. When one of the parties in the experiment performs measures using commuting observables, this upper-bound remains valid.
4. Otherwise, the upper-bound of this score is $2\sqrt{2}$, regardless of the observables that are used and the quantum state that is measured, and
5. This upper-bound is reached for a suitable choice of observables when measuring the Bell state.

### License

BSD License

### Topics

- Mathematics/Algebra
- Mathematics/Physics/Quantum information

### Session TsirelsonBound

- Tensor_Mat_Compl_Properties
- Matrix_L2_Operator_Norm
- Density_Matrix_Basics
- Tsirelson

### Depends on

- Simultaneous diagonalization of pairwise commuting Hermitian matrices

## Cite

×

TsirelsonBound-AFP

    @article{TsirelsonBound-AFP,
      author  = {Mnacho Echenim and Mehdi Mhalla and Coraline Mori},
      title   = {The CHSH inequality: Tsirelson's upper-bound and other results},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/TsirelsonBound.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- May 17, 2023 : Isabelle2022