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
- Bell nonlocality
Nicolas Brunner, Daniel Cavalcanti, Stefano Pironio, Valerio Scarani, Stephanie Wehner, 2013
Lean context
- Import
QIT.Nonlocality.Bell- Lean declaration
QIT.Bell.CHSH.value_eq_correlators
Copy a short prompt with the import, Lean declaration, citations, and public source link.