Tailored game descriptions, read as games of the foundations

MIPRE/TailoredGameValue.lean states TMIP* = RE in the self-contained vocabulary of MIPRE.HaltingGameValue: its games are HaltingGameValue.SynchronousGames, its value the synchronous value HaltingGameValue.gameValue, and its strategies the permutation strategies TailoredGameValue.PermStrategy. This file reads them in the foundations, where the quantum value MIPRE.quantumValue lives, as MIPRE/Foundations/GameDescription.lean does for HaltingGameValue.GameData.

• HaltingGameValue.SynchronousGame.toMIPRE: a synchronous game of the self-contained vocabulary, as a MIPRE.SynchronousGame — the same fields — and gameValue_eq_syncValue, gameValue_le_quantumValue: its synchronous value is MIPRE.syncValue of it, and is at most its quantum value. The strategy repackagings are GameDescription.lean's, for any game.
• TailoredGameData.syncGame, TailoredGameData.game: a tailored game description read so.
• PermStrategy.toSync: a permutation strategy of a description is a synchronous strategy of it, with the same value. Its measurements are the Fourier transforms of commuting self-adjoint involutions — the observables are signed permutation matrices, so self-adjoint once involutive (IsSignedPerm.isHermitian) — hence projective (isPVMIn_fourierProj).
• HasPerfectZPC.gameValue_eq_one, HasPerfectZPC.quantumValue_eq_one: a perfect ZPC strategy gives synchronous and quantum value 1.

noncomputable def HaltingGameValue.SynchronousGame.toMIPRE {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : MIPRE.SynchronousGame X A

The same game, as a MIPRE.SynchronousGame.

Equations

• G.toMIPRE = { μ := G.μ, μ_nonneg := ⋯, μ_sum_one := ⋯, D := G.D, synchronous := ⋯ }

noncomputable def HaltingGameValue.SynchronousGame.toSyncStrategy {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : SyncStrategy G) : MIPRE.SyncStrategy G.toMIPRE

A synchronous strategy of the self-contained vocabulary, as one of the foundations: the same dimension and operators.

Equations

• G.toSyncStrategy S = { d := S.d, d_pos := ⋯, P := { M := fun (x : X) (a : A) => ↑((S.povm x).mats a), selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ } }

noncomputable def HaltingGameValue.SynchronousGame.ofSyncStrategy {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : MIPRE.SyncStrategy G.toMIPRE) : SyncStrategy G

A synchronous strategy of the foundations, in the self-contained vocabulary.

Equations

• G.ofSyncStrategy S = { d := S.d, d_pos := ⋯, povm := fun (x : X) => { mats := (S.povm x).mats, nonneg := ⋯, normalized := ⋯ }, projective := ⋯ }

theorem HaltingGameValue.SynchronousGame.value_toSyncStrategy {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : SyncStrategy G) : (G.toSyncStrategy S).value = strategyValue G S

theorem HaltingGameValue.SynchronousGame.strategyValue_ofSyncStrategy {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : MIPRE.SyncStrategy G.toMIPRE) : strategyValue G (G.ofSyncStrategy S) = S.value

theorem HaltingGameValue.SynchronousGame.strategyValue_nonneg {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : SyncStrategy G) : 0 ≤ strategyValue G S

theorem HaltingGameValue.SynchronousGame.strategyValue_le_one {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (S : SyncStrategy G) : strategyValue G S ≤ 1

theorem HaltingGameValue.SynchronousGame.bddAbove_range_strategyValue {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : BddAbove (Set.range fun (S : SyncStrategy G) => strategyValue G S)

theorem HaltingGameValue.SynchronousGame.gameValue_nonneg {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : 0 ≤ gameValue G

theorem HaltingGameValue.SynchronousGame.gameValue_eq_syncValue {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : gameValue G = MIPRE.syncValue G.toMIPRE

The two synchronous values agree.

theorem HaltingGameValue.SynchronousGame.gameValue_le_quantumValue {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : gameValue G ≤ MIPRE.quantumValue G.toMIPRE.toGame

The synchronous value is at most the quantum value (lem:sync-le-valstar).

theorem TailoredGameValue.signedPermMatrix_eq {m : ℕ} (σ : Equiv.Perm (Fin m)) (s : Fin m → Bool) : signedPermMatrix σ s = MIPRE.Tailored.signedPermMatrix σ s

The signed permutation matrices of the self-contained statement are the library's.

@[reducible, inline]

noncomputable abbrev TailoredGameValue.TailoredGameData.syncGame (g : TailoredGameData) : MIPRE.SynchronousGame (Fin (g.nV + 1)) (Fin g.ansLen → Bool)

A tailored game description, as a synchronous game of the foundations.

Equations

• g.syncGame = g.toGame.toMIPRE

@[reducible, inline]

noncomputable abbrev TailoredGameValue.TailoredGameData.game (g : TailoredGameData) : MIPRE.Game (Fin (g.nV + 1)) (Fin (g.nV + 1)) (Fin g.ansLen → Bool) (Fin g.ansLen → Bool)

A tailored game description, as a two-player game of the foundations.

Equations

• g.game = g.syncGame.toGame

theorem TailoredGameValue.TailoredGameData.gameValue_le_quantumValue (g : TailoredGameData) : HaltingGameValue.gameValue g.toGame ≤ MIPRE.quantumValue g.game

theorem TailoredGameValue.PermStrategy.proj_eq {g : TailoredGameData} (S : PermStrategy g) (x : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : S.proj x a = MIPRE.Tailored.fourierProj (S.U x) a

The measurements are the library's Fourier transforms of the observables.

theorem TailoredGameValue.PermStrategy.star_U {g : TailoredGameData} (S : PermStrategy g) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : star (S.U x i) = S.U x i

The observables are self-adjoint: involutive signed permutation matrices.

theorem TailoredGameValue.PermStrategy.isPVMIn_proj {g : TailoredGameData} (S : PermStrategy g) (x : Fin (g.nV + 1)) : MIPRE.IsPVMIn (S.proj x)

The measurements are projective.

noncomputable def TailoredGameValue.PermStrategy.toSync {g : TailoredGameData} (S : PermStrategy g) : MIPRE.SyncStrategy g.syncGame

A permutation strategy is a synchronous strategy, with the same dimension and the Fourier transforms as its measurements.

Equations

• S.toSync = { d := S.m, d_pos := ⋯, P := { M := S.proj, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ } }

theorem TailoredGameValue.PermStrategy.value_toSync {g : TailoredGameData} (S : PermStrategy g) : S.toSync.value = S.value

It has the same value.

theorem TailoredGameValue.TailoredGameData.HasPerfectZPC.syncValue_eq_one {g : TailoredGameData} (h : g.HasPerfectZPC) : MIPRE.syncValue g.syncGame = 1

A perfect ZPC strategy gives synchronous value 1 in the foundations.

theorem TailoredGameValue.TailoredGameData.HasPerfectZPC.gameValue_eq_one {g : TailoredGameData} (h : g.HasPerfectZPC) : HaltingGameValue.gameValue g.toGame = 1

A perfect ZPC strategy gives synchronous value 1.

theorem TailoredGameValue.TailoredGameData.HasPerfectZPC.quantumValue_eq_one {g : TailoredGameData} (h : g.HasPerfectZPC) : MIPRE.quantumValue g.game = 1

A perfect ZPC strategy gives quantum value 1.