2023/06/21 by Mnacho Echenim, Mehdi Mhalla, Echenim, Mnacho +1
Computer Science · Mathematics · Physics and Astronomy · #Bell test experiments #Bell's theorem #CHSH inequality #Calculus (dental) #Discrete mathematics #Einstein #FOS: Computer and information sciences #FOS: Physical sciences #Hidden variable theory #Inequality #Logic in Computer Science (cs.LO) #Mathematical analysis #Mathematical physics #Mathematics #Physics #Pure mathematics #Quantum #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum Mechanics and Applications #Quantum Physics (quant-ph) #Quantum mechanics #Theoretical physics #Upper and lower bounds
paper · pdf · doi:10.48550/arxiv.2306.12535
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2023/06/21 · openalex created_date 2023/06/24 · openalex updated_date 2026/08/01
We present a formalization of several fundamental notions and results from Quantum Information theory, including density matrices and projective measurements, along with the proof that the local hidden-variable hypothesis advocated by Einstein to model quantum mechanics cannot hold. The proof of the latter result is based on the so-called CHSH inequality, and it is the violation of this inequality that was experimentally evidenced by Aspect who earned the Nobel Prize in 2022 for his work. We also formalize various results related to the violation of the CHSH inequality, such as Tsirelson's bound which permits to obtain the maximum violation of this inequality in a quantum setting.