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.

翻译：本文提出了量子信息理论中若干基本概念与结果的形式化，包括密度矩阵与投影测量，同时给出了爱因斯坦为建立量子力学模型所倡导的局域隐变量假说不成立的证明。后者基于所谓的CHSH不等式，正是该不等式的违背被阿斯佩克特通过实验证实，并因此荣获2022年诺贝尔奖。我们还形式化了与CHSH不等式违背相关的若干结果，例如在量子框架下获得该不等式最大违背值的Tsirelson界。