Nonlocality and certification / Bound
CHSH functional and classical bound (value <= 2)
Bound statement
For every CHSH behavior $p$ with binary outcome signs $a$ and $b$, if $p$ admits a local hidden-variable decomposition, then the CHSH functional $S(p)=\langle a_0b_0\rangle_p+\langle a_0b_1\rangle_p+\langle a_1b_0\rangle_p-\langle a_1b_1\rangle_p$ satisfies $S(p)\le2$.
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_le_two_of_isLocal
Copy a short prompt with the import, Lean declaration, citations, and public source link.