Bipartite correlation sets C_q, C_qa, C_qc

The three sets of bipartite correlations p : X → Y → A → B → ℝ of Tsirelson's problem (blueprint cor:tsirelson):

• Cq X Y A B, the Born probabilities of finite-dimensional tensor-product strategies, with the projective measurements of MIPRE.TensorProductStrategy;
• Cqa X Y A B := closure (Cq X Y A B), in the product topology;
• Cqc X Y A B, the correlations of commuting-operator strategies (MIPRE.CommutingOperatorStrategy, POVMs on a Hilbert space in universe 0).

A game pays off linearly in a correlation (Game.payoff), and the values of both strategy classes are that payoff (TensorProductStrategy.value_eq_payoff, CommutingOperatorStrategy.value_eq_payoff). Every tensor-product strategy is a commuting-operator strategy on ℂ^dA ⊗ ℂ^dB (TensorProductStrategy.toCommuting), so Cq ⊆ Cqc and quantumValue ≤ commutingOperatorValue; payoffs on Cqa are bounded by the quantum value, since the payoff is continuous. Cqa ⊆ Cqc holds as soon as Cqc is closed.

The commuting-operator correlations are nonnegative and sum to one for each question pair (CommutingOperatorStrategy.correlation_nonneg, correlation_sum), by Mathlib's Commute.mul_nonneg: the product of two commuting positive operators is positive. So the commuting-operator value lies in [0, 1].

The payoff of a correlation

noncomputable def MIPRE.Game.payoff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (p : X → Y → A → B → ℝ) : ℝ

The payoff of a correlation p in the game G: the probability of winning when the answers (a, b) to the questions (x, y) are drawn with probability p x y a b.

Equations

• G.payoff p = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, (G.μ x y * if G.D x y a b = true then 1 else 0) * p x y a b

theorem MIPRE.Game.continuous_payoff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Continuous G.payoff

The payoff is continuous in the correlation.

Tensor-product correlations

noncomputable def MIPRE.TensorProductStrategy.correlation {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : X → Y → A → B → ℝ

The correlation of a tensor-product strategy: its Born-rule probabilities ⟨ψ| A^x_a ⊗ B^y_b |ψ⟩.

Equations

• S.correlation x y a b = (star S.ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (S.PA.M x a) (S.PB.M y b)).mulVec S.ψ).re

theorem MIPRE.TensorProductStrategy.value_eq_payoff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : S.value = G.payoff S.correlation

The value of a tensor-product strategy is the payoff of its correlation.

@[simp]

theorem MIPRE.TensorProductStrategy.correlation_copy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X Y A B) : (S.copy G').correlation = S.correlation

The correlation does not depend on the game the strategy is attached to.

def MIPRE.Cq (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype A] [Fintype B] : Set (X → Y → A → B → ℝ)

C_q: the correlations of finite-dimensional tensor-product strategies. The game is immaterial (TensorProductStrategy only carries it as an index), so the definition quantifies over the strategy data directly; mem_Cq_iff restates it for any game.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.Cqa (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype A] [Fintype B] : Set (X → Y → A → B → ℝ)

C_qa: the closure of C_q.

Equations

• MIPRE.Cqa X Y A B = closure (MIPRE.Cq X Y A B)

theorem MIPRE.TensorProductStrategy.correlation_mem_Cq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : S.correlation ∈ Cq X Y A B

The correlation of a tensor-product strategy lies in C_q.

theorem MIPRE.mem_Cq_iff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {p : X → Y → A → B → ℝ} : p ∈ Cq X Y A B ↔ ∃ (S : TensorProductStrategy G), S.correlation = p

Membership in C_q, through the strategies of any game on the same alphabets.

theorem MIPRE.payoff_le_quantumValue_of_mem_Cq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {p : X → Y → A → B → ℝ} (hp : p ∈ Cq X Y A B) : G.payoff p ≤ quantumValue G

The payoff of a quantum correlation is at most the quantum value.

theorem MIPRE.payoff_le_quantumValue_of_mem_Cqa {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {p : X → Y → A → B → ℝ} (hp : p ∈ Cqa X Y A B) : G.payoff p ≤ quantumValue G

The payoff of a correlation in C_qa is at most the quantum value: the payoff is continuous, so the bound passes to the closure.

Commuting-operator correlations

theorem MIPRE.CommutingOperatorStrategy.value_eq_payoff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : value G S = G.payoff S.correlation

The value of a commuting-operator strategy is the payoff of its correlation.

theorem MIPRE.CommutingOperatorStrategy.isPositive_mul {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : (S.E x a * S.F y b).IsPositive

The joint effect E^x_a F^y_b is a positive operator: the product of two commuting positive operators.

theorem MIPRE.CommutingOperatorStrategy.correlation_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : 0 ≤ S.correlation x y a b

Commuting-operator correlations are nonnegative.

theorem MIPRE.CommutingOperatorStrategy.correlation_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) : ∑ a : A, ∑ b : B, S.correlation x y a b = 1

For each question pair, commuting-operator correlations sum to one.

theorem MIPRE.CommutingOperatorStrategy.value_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : 0 ≤ value G S

The value of a commuting-operator strategy is nonnegative.

theorem MIPRE.CommutingOperatorStrategy.value_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : value G S ≤ 1

The value of a commuting-operator strategy is at most one.

theorem MIPRE.CommutingOperatorStrategy.bddAbove_range_value {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : BddAbove (Set.range fun (S : CommutingOperatorStrategy X Y A B) => value G S)

The values of commuting-operator strategies are bounded above (by one).

theorem MIPRE.CommutingOperatorStrategy.value_le_commutingOperatorValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : CommutingOperatorStrategy X Y A B) : value G S ≤ commutingOperatorValue G

A strategy's value is at most the commuting-operator value.

theorem MIPRE.commutingOperatorValue_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : 0 ≤ commutingOperatorValue G

The commuting-operator value is nonnegative.

theorem MIPRE.commutingOperatorValue_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : commutingOperatorValue G ≤ 1

The commuting-operator value is at most one.

def MIPRE.Cqc (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Set (X → Y → A → B → ℝ)

C_qc: the correlations of commuting-operator strategies.

Equations

• MIPRE.Cqc X Y A B = Set.range fun (S : MIPRE.CommutingOperatorStrategy X Y A B) => S.correlation

theorem MIPRE.payoff_le_commutingOperatorValue_of_mem_Cqc {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {p : X → Y → A → B → ℝ} (hp : p ∈ Cqc X Y A B) : G.payoff p ≤ commutingOperatorValue G

The payoff of a commuting-operator correlation is at most the commuting-operator value.

Tensor-product strategies are commuting-operator strategies

theorem MIPRE.TensorProductStrategy.isPositive_toEuclideanCLM {n : Type u_5} [Fintype n] [DecidableEq n] {P : Matrix n n ℂ} (hs : star P = P) (hp : P * P = P) : (Matrix.toEuclideanCLM P).IsPositive

A projection on Euclidean space, as the image of a self-adjoint idempotent matrix, is a positive operator.

theorem MIPRE.TensorProductStrategy.kronecker_sum_left {m : Type u_5} {n : Type u_6} {ι : Type u_7} (s : Finset ι) (P : ι → Matrix m m ℂ) (Q : Matrix n n ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (∑ i ∈ s, P i) Q = ∑ i ∈ s, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P i) Q

theorem MIPRE.TensorProductStrategy.kronecker_sum_right {m : Type u_5} {n : Type u_6} {ι : Type u_7} (s : Finset ι) (P : Matrix m m ℂ) (Q : ι → Matrix n n ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P (∑ i ∈ s, Q i) = ∑ i ∈ s, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P (Q i)

noncomputable def MIPRE.TensorProductStrategy.ofTensor {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA dB : ℕ} (ψ : Fin dA × Fin dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (PA : ProjectiveMeasurement X A (Matrix (Fin dA) (Fin dA) ℂ)) (PB : ProjectiveMeasurement Y B (Matrix (Fin dB) (Fin dB) ℂ)) : CommutingOperatorStrategy X Y A B

Finite-dimensional tensor-product data as a commuting-operator strategy, on the Euclidean space ℂ^(dA × dB): the first player measures A^x_a ⊗ 1, the second 1 ⊗ B^y_b.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.TensorProductStrategy.correlation_ofTensor {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA dB : ℕ} (ψ : Fin dA × Fin dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (PA : ProjectiveMeasurement X A (Matrix (Fin dA) (Fin dA) ℂ)) (PB : ProjectiveMeasurement Y B (Matrix (Fin dB) (Fin dB) ℂ)) : (ofTensor ψ hψ PA PB).correlation = fun (x : X) (y : Y) (a : A) (b : B) => (star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (PA.M x a) (PB.M y b)).mulVec ψ).re

The embedding preserves the Born probabilities.

noncomputable def MIPRE.TensorProductStrategy.toCommuting {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : CommutingOperatorStrategy X Y A B

A tensor-product strategy is a commuting-operator strategy.

Equations

• S.toCommuting = MIPRE.TensorProductStrategy.ofTensor S.ψ ⋯ S.PA S.PB

theorem MIPRE.TensorProductStrategy.correlation_toCommuting {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : S.toCommuting.correlation = S.correlation

The embedding preserves the correlation.

theorem MIPRE.TensorProductStrategy.value_toCommuting {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : CommutingOperatorStrategy.value G S.toCommuting = S.value

The embedding preserves the value.

theorem MIPRE.Cq_subset_Cqc {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Cq X Y A B ⊆ Cqc X Y A B

C_q ⊆ C_qc.

theorem MIPRE.quantumValue_le_commutingOperatorValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : quantumValue G ≤ commutingOperatorValue G

The quantum value is at most the commuting-operator value.

theorem MIPRE.Cqa_subset_Cqc_of_isClosed {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (h : IsClosed (Cqc X Y A B)) : Cqa X Y A B ⊆ Cqc X Y A B

C_qa ⊆ C_qc once C_qc is closed.