We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors that is frequently used in quantum computing. We also formalize the CHSH inequality, a result that holds on arbitrary probability spaces, which can used to disprove the existence of a local hidden-variable theory for quantum mechanics.
翻译:我们在Isabelle/HOL中提出了量子投射测量的正规化,这是一个涉及在量子计算中经常使用的正向投射器的测量类别。 我们还正式确定了CHSH的不平等,这一结果维持了任意概率空间,这可用来推翻本地的量子力学隐性可变理论的存在。