Bipartite commuting-operator strategies and the commuting-operator value

A commuting-operator strategy for a (not necessarily synchronous) game (blueprint def:co-strategy-bipartite): a complex Hilbert space H, a unit vector ψ, and POVM families E x (first player) and F y (second player) of positive operators summing to one, with every E x a commuting with every F y b. Its value in a game and the commuting-operator value valco(G) of the game (blueprint def:co-value-bipartite) are the usual ones.

This is the two-prover picture of the commuting-operator model. The synchronous, tracial commuting strategies of MIPRE.Foundations.Games (CommutingStrategy, commValue) are the picture used by the compression pipeline; the two agree for synchronous games only up to the rounding of almost-synchronous correlations (blueprint thm:almost-sync), which is why both are defined. The definitions mirror those of the vendored development MIPRE/Background/Repetition/CommutingRepetition/ field by field, so that its theorems transfer by a field-by-field identification.

The Hilbert space lives in universe 0; by restriction to the separable subspace cyclically generated by ψ under the finitely many effects this loses no generality.

structure MIPRE.CommutingOperatorStrategy (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type (max (max (max (max 1 u_1) u_2) u_3) u_4)

A commuting-operator strategy over question alphabets X, Y and answer alphabets A, B (blueprint def:co-strategy-bipartite).

• H : Type

  The Hilbert space.

• normedAddCommGroup : NormedAddCommGroup self.H
• innerProductSpace : InnerProductSpace ℂ self.H
• completeSpace : CompleteSpace self.H
• ψ : self.H

  The shared state.

• ψ_norm : ‖self.ψ‖ = 1

  The shared state is a unit vector.

• E : X → A → self.H →L[ℂ] self.H

  The first player's measurement operators.

• F : Y → B → self.H →L[ℂ] self.H

  The second player's measurement operators.

• E_pos (x : X) (a : A) : (self.E x a).IsPositive

  The first player's operators are positive.

• F_pos (y : Y) (b : B) : (self.F y b).IsPositive

  The second player's operators are positive.

• E_sum (x : X) : ∑ a : A, self.E x a = 1

  The first player's operators form a POVM for each question.

• F_sum (y : Y) : ∑ b : B, self.F y b = 1

  The second player's operators form a POVM for each question.

• commutes (x : X) (y : Y) (a : A) (b : B) : Commute (self.E x a) (self.F y b)

  The two players' operators commute.

noncomputable def MIPRE.CommutingOperatorStrategy.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] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : ℝ

The probability that the players answer (a, b) to the questions (x, y): ⟨ψ| E^x_a F^y_b |ψ⟩, a real number since the commuting product of two positive operators is self-adjoint; we take the real part so that the definition carries no proof obligations.

Equations

• S.correlation x y a b = (inner ℂ S.ψ ((S.E x a) ((S.F y b) S.ψ))).re

noncomputable def MIPRE.CommutingOperatorStrategy.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) (S : CommutingOperatorStrategy X Y A B) : ℝ

The value of a commuting-operator strategy in the game G.

Equations

• MIPRE.CommutingOperatorStrategy.value G S = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, (G.μ x y * if G.D x y a b = true then 1 else 0) * S.correlation x y a b

noncomputable def MIPRE.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) : ℝ

The commuting-operator value valco(G) of a game (blueprint def:co-value-bipartite): the supremum of strategy values over all commuting-operator strategies.

Equations

• MIPRE.commutingOperatorValue G = ⨆ (S : MIPRE.CommutingOperatorStrategy X Y A B), MIPRE.CommutingOperatorStrategy.value G S