Theorems · Theorem · functional analysis

tsirelson_inequality

∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : Algebra ℝ R] [IsOrderedModule ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R),
  IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

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!)

Defined in

Mathlib.Algebra.Star.CHSH

Cited by

0 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingPartialOrderStarRingStarOrderedRingAlgebraIsOrderedModuleStarModule