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

• ObservableStrategy: 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 ObservableStrategy (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)

structure BipartiteObservableStrategy (n : Type u_1) [Fintype n] [DecidableEq n] (G : LCSLayout) : Type u_1

• obs : Fin G.s → Matrix n n ℂ
• is_observable (j : Fin G.s) : IsObservable (self.obs j)
• sameEquation_comm (i : Fin G.r) : Pairwise fun (j k : ↥(G.V i)) => Commute (self.obs ↑j) (self.obs ↑k)

noncomputable def BipartiteObservableStrategy.toObservableStrategy {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (strat : BipartiteObservableStrategy n G) : ObservableStrategy (Matrix (n × n) (n × n) ℂ) G

Equations

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

@[simp]

theorem BipartiteObservableStrategy.alice_obs_eq {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (strat : BipartiteObservableStrategy n G) (j : Fin G.s) : strat.toObservableStrategy.alice_obs j = bipartiteAliceLift (strat.obs j)

@[simp]

theorem BipartiteObservableStrategy.bob_obs_eq {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (strat : BipartiteObservableStrategy n G) (j : Fin G.s) : strat.toObservableStrategy.bob_obs j = bipartiteBobLift (strat.obs j)

@[simp]

theorem BipartiteObservableStrategy.alice_observable_eq {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (strat : BipartiteObservableStrategy n G) (j : Fin G.s) : ⋯ = ⋯

@[simp]

theorem BipartiteObservableStrategy.bob_observable_eq {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (strat : BipartiteObservableStrategy n G) (j : Fin G.s) : ⋯ = ⋯

@[simp]

theorem BipartiteObservableStrategy.sameEquation_comm_eq {n : Type u_1} [Fintype n] [DecidableEq n] {G : LCSLayout} (strat : BipartiteObservableStrategy n G) (i : Fin G.r) (j k : ↥(G.V i)) (hjk : j ≠ k) : ⋯ = ⋯