Observable-based Strategy for LCS Games

This module defines the data structure for a strategy in a Linear Constraint System (LCS) game using the observable formalism. In this formalism, players choose observables (self-adjoint involutive operators) instead of projectors.

Key Definitions

• ObservableStrategyData: The data representing an observable strategy, including:
  • alice_obs, bob_obs: The observables for Alice and Bob.
  • sameEquation_comm: The local commutativity of Alice's observables within an equation.
  • alice_bob_commute: The global commutativity between Alice's and Bob's observables.

structure ObservableStrategyData (R : Type u_1) [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (G : LCSLayout) : Type u_1

• alice_obs : Fin G.s → R
• bob_obs : Fin G.s → R
• alice_observable (j : Fin G.s) : IsObservable (self.alice_obs j)
• bob_observable (j : Fin G.s) : IsObservable (self.bob_obs j)
• sameEquation_comm (i : Fin G.r) : Pairwise fun (j k : ↥(G.V i)) => Commute (self.alice_obs ↑j) (self.alice_obs ↑k)
• alice_bob_commute (j k : Fin G.s) : Commute (self.alice_obs j) (self.bob_obs k)

def bipartiteAliceLift {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℂ) : Matrix (n × n) (n × n) ℂ

Equations

• bipartiteAliceLift M = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1

def bipartiteBobLift {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℂ) : Matrix (n × n) (n × n) ℂ

Equations

• bipartiteBobLift M = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M

theorem bipartiteAliceLift_observable {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (h : IsObservable M) : IsObservable (bipartiteAliceLift M)

theorem bipartiteBobLift_observable {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (h : IsObservable M) : IsObservable (bipartiteBobLift M)

theorem bipartite_alice_bob_commute {n : Type u_1} [Fintype n] [DecidableEq n] (M N : Matrix n n ℂ) : Commute (bipartiteAliceLift M) (bipartiteBobLift N)

theorem bipartiteAliceLift_commute {n : Type u_1} [Fintype n] [DecidableEq n] {M N : Matrix n n ℂ} (h : Commute M N) : Commute (bipartiteAliceLift M) (bipartiteAliceLift N)

noncomputable def BipartiteObservableStrategy {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (obs : Fin G.s → Matrix n n ℂ) (obs_is_observable : ∀ (j : Fin G.s), IsObservable (obs j)) (sameEquation_comm : ∀ (i : Fin G.r), Pairwise fun (j k : ↥(G.V i)) => Commute (obs ↑j) (obs ↑k)) : ObservableStrategyData (Matrix (n × n) (n × n) ℂ) G

Equations

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