English
In a noncommutative ordered *-algebra over ℝ, Tsirelson's bound states A0 B0 + A0 B1 + A1 B0 − A1 B1 ≤ √2^3 · 1, with a sum-of-squares decomposition proving the bound.
Русский
В некоммутативной упорядоченной *-алгебре над ℝ Цирелсонова граница задаёт предел: A0 B0 + A0 B1 + A1 B0 − A1 B1 ≤ (√2)^3 · 1, что доказывается разложением на сумму квадратов.
LaTeX
$$$A_0 B_0 + A_0 B_1 + A_1 B_0 - A_1 B_1 \\le \\sqrt{2}^3 \\cdot 1.$$$
Lean4
/-- In a noncommutative ordered `*`-algebra over ℝ,
Tsirelson's bound for a CHSH tuple (A₀, A₁, B₀, B₁) is
`A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2^(3/2) • 1`.
We prove this by providing an explicit sum-of-squares decomposition
of the difference.
(We could work over `ℤ[2^(1/2), 2^(-1/2)]` if we really wanted to!)
-/
theorem tsirelson_inequality [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R]
[IsOrderedModule ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R) (T : IsCHSHTuple A₀ A₁ B₀ B₁) :
A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • (1 : R) := by
-- abel will create `ℤ` multiplication. We will `simp` them away to `ℝ` multiplication.
have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by
rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]
let P := (√2)⁻¹ • (A₁ + A₀) - B₀
let Q := (√2)⁻¹ • (A₁ - A₀) + B₁
have w : √2 ^ 3 • (1 : R) - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2) :=
by
dsimp [P, Q]
-- distribute out all the powers and products appearing on the RHS
simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
-- pull all coefficients out to the front, and combine `√2`s where possible
simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
-- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
-- move Aᵢ to the left of Bᵢ
simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
-- collect terms, simplify coefficients, and collect terms again:
abel_nf
-- all terms coincide, but the last one. Simplify all other terms
simp only [M]
simp only [neg_mul, mul_inv_cancel_of_invertible, add_assoc, add_comm, add_left_comm, one_smul, Int.cast_neg,
neg_smul, Int.cast_ofNat, ← add_smul]
have : √2 ^ 2 = 2 := by norm_num
grind
have pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2) :=
by
have P_sa : star P = P := by
simp only [P, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa]
have Q_sa : star Q = Q := by
simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₁_sa]
have P2_nonneg : 0 ≤ P ^ 2 := by simpa only [P_sa, sq] using star_mul_self_nonneg P
have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
positivity
apply le_of_sub_nonneg
simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos
