Nonlocality and certification / Theorem

CHSH value as a four-correlator expression

Theorem statement

For a bipartite behavior $p(a,b \mid x,y)$ with inputs $x,y \in \{0,1\}$ and outcomes $a,b \in \{-1,1\}$, the CHSH value is \[ S(p) = \langle a_0 b_0 \rangle + \langle a_0 b_1 \rangle + \langle a_1 b_0 \rangle - \langle a_1 b_1 \rangle, \] where $\langle a_x b_y \rangle := \sum_{a,b} ab \, p(a,b \mid x,y)$ is the correlator for settings $x$ and $y$.

Sources

  1. Bell nonlocality

    Nicolas Brunner, Daniel Cavalcanti, Stefano Pironio, Valerio Scarani, Stephanie Wehner, 2013

Lean context

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source