Games, strategies, and values

This file contains the definitions of blueprint Section 2.1 ("Games, strategies, and values") of the MIP* = RE formalization project: two-player one-round nonlocal games, the three classes of strategies (tensor-product, synchronous, and commuting), the associated values, and the entanglement requirement.

The three strategy classes are built on a common skeleton, which this file factors out: a question-indexed family of projective measurements in a complex star algebra (MIPRE.ProjectiveMeasurement). Tensor-product strategies instantiate it on two matrix algebras joined by a state vector and the Born rule; synchronous strategies instantiate it on one matrix algebra ℂ^{d×d}, evaluated against the dimension-normalized trace; commuting strategies are the general case of an abstract unital C*-algebra with a tracial state (MIPRE.TracialState), evaluated by the generic value MIPRE.tracialValue. The inclusion of synchronous into commuting strategies is MIPRE.SyncStrategy.toCommutingStrategy, which preserves the value definitionally; the comparison of values (blueprint lem:sync-le-valco) follows.

The matrix-based definitions (POVM, SynchronousGame, and the synchronous value) agree with those of MIPRE.HaltingGameValue, which is kept self-contained. The synchronous strategy is packaged differently there (with POVMs in place of a ProjectiveMeasurement); MIPRE.SyncStrategy.ofPOVM and MIPRE.SyncStrategy.value_eq provide the correspondence.

Main definitions

• MIPRE.Game: two-player one-round games (blueprint def:game).
• MIPRE.SynchronousGame: synchronous games, with the interpretation MIPRE.SynchronousGame.toGame (blueprint def:sync-game).
• MIPRE.ProjectiveMeasurement: question-indexed projective measurement families in a star ring, the common skeleton of the three strategy classes.
• MIPRE.TracialState: tracial states on a complex star algebra; MIPRE.normalizedTrace is the normalized matrix trace Tr(·)/d.
• MIPRE.tracialValue: the generic value of a projective measurement family against a tracial state.
• MIPRE.POVM: positive operator-valued measures, following the QuantumLib (Lean-QuantumInfo) definition; the vocabulary of the distance measures (MIPRE.Foundations.Distances) and of the correspondence with MIPRE.HaltingGameValue.
• MIPRE.TensorProductStrategy: finite-dimensional tensor-product strategies, with projective measurements on both factors (blueprint def:tensor-strategy).
• MIPRE.quantumValue: the quantum value val* of a game (blueprint def:q-value).
• MIPRE.SyncStrategy: synchronous strategies (blueprint def:sync-strategy), the instantiation of the skeleton at ℂ^{d×d} with the normalized trace.
• MIPRE.SyncStrategy.IsPCC: PCC (projective, consistent, and commuting) strategies (blueprint def:pcc).
• MIPRE.syncValue: the synchronous value of a synchronous game (blueprint def:sync-value).
• MIPRE.CommutingStrategy: commuting strategies, given by a unital C*-algebra with a tracial state (blueprint def:commuting-strategy).
• MIPRE.commValue: the commuting value of a synchronous game (blueprint def:commuting-value).
• MIPRE.SyncStrategy.toCommutingStrategy: a synchronous strategy is a commuting strategy, with the same value (MIPRE.SyncStrategy.value_toCommutingStrategy).
• MIPRE.entRequirement: the entanglement requirement Ent(G, ν) (blueprint def:ent).

Main statements

• MIPRE.tracialValue_nonneg and MIPRE.tracialValue_le_one: the generic value lies in [0, 1]; the synchronous and commuting values inherit both bounds.
• MIPRE.ProjectiveMeasurement.consistency: against a tracial state, a projective family answers equal questions with equal answers (probability zero for a ≠ b).
• MIPRE.syncValue_le_quantumValue: the synchronous value lower-bounds the quantum value (blueprint lem:sync-le-valstar).
• MIPRE.syncValue_le_commValue: the synchronous value lower-bounds the commuting value (blueprint lem:sync-le-valco).

Implementation notes

• Question distributions are bare real-valued functions with nonnegativity and normalization fields, rather than PMF (which is ℝ≥0∞-valued and would force coercions in the value definitions).
• Outcome probabilities are nonnegative reals, but proving so requires positivity arguments; as in MIPRE.HaltingGameValue, each value takes the real part .re of the relevant complex quantity so that the definitions carry no proof obligations.
• The shared layer (ProjectiveMeasurement, TracialState, tracialValue) requires no norm: the definitions and the basic lemmas hold over any complex star algebra. The C*-structure enters only in CommutingStrategy, following the blueprint. In particular the matrix-based strategies never need mathlib's (scoped) matrix operator-norm instances.
• Tensor-product strategies are defined with projective measurements, as in JNVWY (where strategies are assumed projective; by Naimark dilation this loses no generality, and allowing general POVMs would define the same quantum value — a fact we do not need and do not formalize). General POVMs remain as POVM, the vocabulary of the distance measures and rounding arguments.
• The algebra of a CommutingStrategy lives in universe 0. This loses no generality: for a finite game, the GNS representation of the (separable) C*-subalgebra generated by the finitely many measurement operators realizes the same correlation, and it lives in universe 0.
• SyncStrategy.toCommutingStrategy realizes the matrix algebra as CStarMatrix (Fin d) (Fin d) ℂ, mathlib's type synonym of Matrix carrying the (unscoped) operator-norm CStarAlgebra instance. All algebraic instances of CStarMatrix are definitionally those of Matrix, so the strategy transported along CStarMatrix.ofMatrixStarAlgEquiv has the same value by rfl.
• A commuting strategy whose algebra is finite-dimensional is not literally a synchronous strategy: a finite-dimensional C*-algebra is a direct sum of matrix blocks, and its tracial states are the convex combinations of the normalized traces of the blocks. The two notions give the same supremum of values (decompose the trace and pick the best block), but we do not need this fact; the inclusion SyncStrategy.toCommutingStrategy is the direction the project uses.
• POVM matches the QuantumLib (Lean-QuantumInfo) definition (QuantumInfo.Finite.POVM), with selfAdjoint (Matrix d d ℂ) spelled out for its definitionally equal HermitianMat d ℂ, so that the strategy layer can be upstreamed. SyncStrategy.povm and SyncStrategy.ofPOVM convert between the ProjectiveMeasurement packaging and the POVM packaging.

References

• Ji, Natarajan, Vidick, Wright, Yuen, MIP* = RE, arXiv:2001.04383.

Games

structure MIPRE.Game (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 u_1 u_2) u_3) u_4)

A two-player one-round game (blueprint def:game): finite question alphabets X, Y, finite answer alphabets A, B, a probability distribution μ on X × Y, and a decision predicate D (true = accept).

• μ : X → Y → ℝ

  The probability that the players are asked the question pair (x, y).

• μ_nonneg (x : X) (y : Y) : 0 ≤ self.μ x y

  Question probabilities are nonnegative.

• μ_sum_one : ∑ x : X, ∑ y : Y, self.μ x y = 1

  Question probabilities sum to one.

• D : X → Y → A → B → Bool

  The decision predicate: D x y a b = true means the answers (a, b) to the questions (x, y) are accepted.

structure MIPRE.SynchronousGame (X : Type u_1) (A : Type u_2) [Fintype X] [Fintype A] [DecidableEq A] : Type (max u_1 u_2)

A synchronous game (blueprint def:sync-game): both players receive questions from the same alphabet and answer from the same alphabet; on equal questions, unequal answers always lose.

• μ : X → X → ℝ

  The probability that the players are asked the question pair (x, y).

• μ_nonneg (x y : X) : 0 ≤ self.μ x y

  Question probabilities are nonnegative.

• μ_sum_one : ∑ x : X, ∑ y : X, self.μ x y = 1

  Question probabilities sum to one.

• D : X → X → A → A → Bool

  The decision predicate: D x y a b = true means the answers (a, b) to the questions (x, y) are accepted.

• synchronous (x : X) (a b : A) : a ≠ b → self.D x x a b = false

  Unequal answers to equal questions are rejected.

def MIPRE.SynchronousGame.toGame {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : Game X X A A

A synchronous game is in particular a game, with Y = X and B = A.

Equations

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

Projective measurement families and tracial states

All strategy classes below are built on a common skeleton: a question-indexed family of projective measurements in a complex star algebra. Tensor-product and synchronous strategies instantiate it on matrix algebras; commuting strategies on an abstract unital C*-algebra, evaluated against a tracial state. The skeleton is defined once, so that the definitions and basic lemmas are shared. No norm is needed at this level of generality.

structure MIPRE.ProjectiveMeasurement (X : Type u_5) (A : Type u_6) (𝒜 : Type u_7) [Fintype A] [Ring 𝒜] [StarRing 𝒜] : Type (max (max u_5 u_6) u_7)

A question-indexed family of projective measurements with outcomes in a star ring 𝒜: for each question x, the operators M x a are self-adjoint idempotents (i.e. orthogonal projections) that sum to one. This is the common skeleton of the strategy classes: tensor-product strategies (TensorProductStrategy) and synchronous strategies (SyncStrategy) instantiate it at matrix algebras, commuting strategies (CommutingStrategy) at an abstract unital C*-algebra.

• M : X → A → 𝒜

  The measurement operators, indexed by questions and answers.

• selfAdjoint (x : X) (a : A) : star (self.M x a) = self.M x a

  Each measurement operator is self-adjoint.

• projective (x : X) (a : A) : self.M x a * self.M x a = self.M x a

  Each measurement operator is idempotent, hence a projection.

• normalized (x : X) : ∑ a : A, self.M x a = 1

  For each question, the measurement operators sum to one.

structure MIPRE.TracialState (𝒜 : Type u_5) [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] extends 𝒜 →ₗ[ℂ] ℂ : Type u_5

A tracial state on a complex star algebra 𝒜: a linear functional that is positive (0 ≤ τ (star m * m), in the order of ℂ), unital (τ 1 = 1), and tracial (τ (m * n) = τ (n * m)). On a unital C*-algebra this is the standard notion of tracial state (blueprint def:commuting-strategy).

• toFun : 𝒜 → ℂ
• map_add' (x y : 𝒜) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℂ) (x : 𝒜) : self.toFun (m • x) = (RingHom.id ℂ) m • self.toFun x
• nonneg' (m : 𝒜) : 0 ≤ self.toLinearMap (star m * m)

  The functional is positive.

• map_one' : self.toLinearMap 1 = 1

  The functional is unital.

• map_mul_comm' (m n : 𝒜) : self.toLinearMap (m * n) = self.toLinearMap (n * m)

  The functional is tracial.

@[instance_reducible]

instance MIPRE.TracialState.instFunLikeComplex {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] : FunLike (TracialState 𝒜) 𝒜 ℂ

Equations

• MIPRE.TracialState.instFunLikeComplex = { coe := fun (τ : MIPRE.TracialState 𝒜) => ⇑τ.toLinearMap, coe_injective := ⋯ }

instance MIPRE.TracialState.instLinearMapClassComplex {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] : LinearMapClass (TracialState 𝒜) ℂ 𝒜 ℂ

@[simp]

theorem MIPRE.TracialState.coe_toLinearMap {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) : ⇑τ.toLinearMap = ⇑τ

@[simp]

theorem MIPRE.TracialState.coe_mk {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (f : 𝒜 →ₗ[ℂ] ℂ) (h₁ : ∀ (m : 𝒜), 0 ≤ f (star m * m)) (h₂ : f 1 = 1) (h₃ : ∀ (m n : 𝒜), f (m * n) = f (n * m)) : ⇑{ toLinearMap := f, nonneg' := h₁, map_one' := h₂, map_mul_comm' := h₃ } = ⇑f

theorem MIPRE.TracialState.star_mul_self_nonneg {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) (m : 𝒜) : 0 ≤ τ (star m * m)

A tracial state is positive.

@[simp]

theorem MIPRE.TracialState.map_one {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) : τ 1 = 1

A tracial state is unital.

theorem MIPRE.TracialState.map_mul_comm {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) (m n : 𝒜) : τ (m * n) = τ (n * m)

A tracial state is tracial.

theorem MIPRE.TracialState.nonneg_mul {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) {p q : 𝒜} (hps : star p = p) (hpp : p * p = p) (hqs : star q = q) (hqq : q * q = q) : 0 ≤ τ (p * q)

The trace of a product of two projections is nonnegative: τ (p * q) = τ (star (q * p) * (q * p)). This is the positivity of outcome probabilities for the strategies below.

theorem MIPRE.TracialState.re_nonneg_mul {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] (τ : TracialState 𝒜) {p q : 𝒜} (hps : star p = p) (hpp : p * p = p) (hqs : star q = q) (hqq : q * q = q) : 0 ≤ (τ (p * q)).re

Real-part form of TracialState.nonneg_mul.

def MIPRE.TracialState.comp {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Module ℂ ℬ] (τ : TracialState ℬ) (φ : 𝒜 ≃⋆ₐ[ℂ] ℬ) : TracialState 𝒜

Pull back a tracial state along a star-algebra equivalence.

Equations

• τ.comp φ = { toFun := fun (m : 𝒜) => τ (φ m), map_add' := ⋯, map_smul' := ⋯, nonneg' := ⋯, map_one' := ⋯, map_mul_comm' := ⋯ }

@[simp]

theorem MIPRE.TracialState.comp_apply {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Module ℂ ℬ] (τ : TracialState ℬ) (φ : 𝒜 ≃⋆ₐ[ℂ] ℬ) (m : 𝒜) : (τ.comp φ) m = τ (φ m)

def MIPRE.ProjectiveMeasurement.map {X : Type u_1} {A : Type u_3} [Fintype A] {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Module ℂ ℬ] (φ : 𝒜 ≃⋆ₐ[ℂ] ℬ) (P : ProjectiveMeasurement X A 𝒜) : ProjectiveMeasurement X A ℬ

Transport a projective measurement family along a star-algebra equivalence.

Equations

• MIPRE.ProjectiveMeasurement.map φ P = { M := fun (x : X) (a : A) => φ (P.M x a), selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.map_M {X : Type u_1} {A : Type u_3} [Fintype A] {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Module ℂ ℬ] (φ : 𝒜 ≃⋆ₐ[ℂ] ℬ) (P : ProjectiveMeasurement X A 𝒜) (x : X) (a : A) : (map φ P).M x a = φ (P.M x a)

theorem MIPRE.ProjectiveMeasurement.consistency {X : Type u_1} {A : Type u_3} [Fintype A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [DecidableEq A] (P : ProjectiveMeasurement X A 𝒜) (τ : TracialState 𝒜) (x : X) {a b : A} (hab : a ≠ b) : τ (P.M x a * P.M x b) = 0

Perfect consistency: against a tracial state, a projective measurement family answers unequal answers to equal questions with probability zero. This is why the "consistent" condition of a PCC strategy (blueprint def:pcc) is automatic for synchronous strategies.

POVMs

structure MIPRE.POVM (X : Type u_7) (d : Type u_8) [Fintype X] [Fintype d] [DecidableEq d] : Type (max u_7 u_8)

A POVM is a (finite) collection of PSD matrices on the same Hilbert space that sum to the identity. Here X indexes the matrices, and d is the space dimension.

This is the QuantumLib (Lean-QuantumInfo) definition of POVM, with selfAdjoint (Matrix d d ℂ) spelled out for its definitionally equal HermitianMat d ℂ; 0 ≤ mats x is the Loewner order, i.e. positive semidefiniteness.

General POVMs are not part of the strategy definitions (strategies are projective, via ProjectiveMeasurement); they are the vocabulary of the distance measures (MIPRE.Foundations.Distances) and of the correspondence with MIPRE.HaltingGameValue (SyncStrategy.povm, SyncStrategy.ofPOVM).

• mats : X → ↥(selfAdjoint (Matrix d d ℂ))

  The measurement operators, one for each outcome.

• nonneg (x : X) : 0 ≤ self.mats x

  Each measurement operator is positive semidefinite.

• normalized : ∑ x : X, self.mats x = 1

  The measurement operators sum to the identity.

Tensor-product strategies and the quantum value

structure MIPRE.TensorProductStrategy {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) : Type (max (max (max u_1 u_2) u_3) u_4)

A tensor-product strategy for a game G (blueprint def:tensor-strategy): finite-dimensional Hilbert spaces ℂ^dA and ℂ^dB, a unit vector ψ in their tensor product — realized as Fin dA × Fin dB → ℂ — and projective measurements {A^x_a} on ℂ^dA and {B^y_b} on ℂ^dB, packaged as ProjectiveMeasurement families on the two matrix algebras. Restricting to projective measurements follows JNVWY; by Naimark dilation this loses no generality. Outcome probabilities are computed using the Born rule (see TensorProductStrategy.value).

• dA : ℕ

  The dimension of the first player's Hilbert space.

• dB : ℕ

  The dimension of the second player's Hilbert space.

• ψ : Fin self.dA × Fin self.dB → ℂ

  The shared state, a vector in the tensor product ℂ^dA ⊗ ℂ^dB = ℂ^(dA × dB).

• ψ_unit : star self.ψ ⬝ᵥ self.ψ = 1

  The shared state is a unit vector. (In particular dA and dB are positive, since a zero-dimensional space contains no unit vector.)

• PA : ProjectiveMeasurement X A (Matrix (Fin self.dA) (Fin self.dA) ℂ)

  The first player's measurements: for each question x, a projective measurement on ℂ^dA.

• PB : ProjectiveMeasurement Y B (Matrix (Fin self.dB) (Fin self.dB) ℂ)

  The second player's measurements: for each question y, a projective measurement on ℂ^dB.

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

The value of a tensor-product strategy in G (blueprint def:q-value): the players answer questions (x, y) with (a, b) with the Born-rule probability ⟨ψ| A^x_a ⊗ B^y_b |ψ⟩, the tensor product being realized by the Kronecker product. The probability is a nonnegative real; we take the real part so that the definition typechecks with no proof obligations.

Equations

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

noncomputable def MIPRE.quantumValue {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 quantum value val*(G) of a game (blueprint def:q-value): the supremum of strategy values over all tensor-product strategies.

Equations

• MIPRE.quantumValue G = ⨆ (S : MIPRE.TensorProductStrategy G), S.value

The generic tracial value

noncomputable def MIPRE.tracialValue {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [DecidableEq A] (G : SynchronousGame X A) (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) : ℝ

The value of a projective measurement family P against a tracial state τ in a synchronous game G: the players answer questions (x, y) with (a, b) with probability τ (M^x_a M^y_b), a nonnegative real by TracialState.nonneg_mul; we take the real part so that the definition carries no proof obligations. The synchronous value (blueprint def:sync-value) and the commuting value (blueprint def:commuting-value) are instantiations.

Equations

• MIPRE.tracialValue G τ P = ∑ x : X, ∑ y : X, ∑ a : A, ∑ b : A, (G.μ x y * if G.D x y a b = true then 1 else 0) * (τ (P.M x a * P.M y b)).re

theorem MIPRE.tracialValue_nonneg {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [DecidableEq A] (G : SynchronousGame X A) (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) : 0 ≤ tracialValue G τ P

The generic value is nonnegative.

theorem MIPRE.tracialValue_le_one {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Module ℂ 𝒜] [DecidableEq A] (G : SynchronousGame X A) (τ : TracialState 𝒜) (P : ProjectiveMeasurement X A 𝒜) : tracialValue G τ P ≤ 1

The generic value is at most one: for each question pair the outcome probabilities τ (M^x_a M^y_b) sum to τ 1 = 1 over the answers.

noncomputable def MIPRE.normalizedTrace (n : Type u_7) [Fintype n] [DecidableEq n] [hn : Nonempty n] : TracialState (Matrix n n ℂ)

The dimension-normalized trace τ(m) = Tr(m)/n is a tracial state on the matrix algebra ℂ^{n×n} (in fact its unique tracial state, though we do not prove this).

Equations

• MIPRE.normalizedTrace n = { toLinearMap := (↑(Fintype.card n))⁻¹ • Matrix.traceLinearMap n ℂ ℂ, nonneg' := ⋯, map_one' := ⋯, map_mul_comm' := ⋯ }

@[simp]

theorem MIPRE.normalizedTrace_apply (n : Type u_7) [Fintype n] [DecidableEq n] [Nonempty n] (m : Matrix n n ℂ) : (normalizedTrace n) m = (↑(Fintype.card n))⁻¹ * m.trace

Synchronous strategies and the synchronous value

structure MIPRE.SyncStrategy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : Type (max u_1 u_3)

A synchronous strategy for a synchronous game (blueprint def:sync-strategy): a question-indexed projective measurement family on ℂ^d (d > 0). Measurements for different questions need not commute. There is no state vector: outcome probabilities are computed with the dimension-normalized trace τ(M) = Tr(M)/d (see SyncStrategy.value). This is the instantiation of the commuting framework at the full matrix algebra with its canonical tracial state, see SyncStrategy.toCommutingStrategy.

• d : ℕ

  The dimension of the Hilbert space.

• d_pos : 0 < self.d

  The dimension is positive.

• P : ProjectiveMeasurement X A (Matrix (Fin self.d) (Fin self.d) ℂ)

  The measurements: for each question, a projective measurement on ℂ^d.

noncomputable def MIPRE.SyncStrategy.value {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : ℝ

The value of a synchronous strategy in G (blueprint def:sync-value): the generic tracial value against the normalized trace τ(M) = Tr(M)/d. See SyncStrategy.value_eq for the explicit form.

Equations

• S.value = MIPRE.tracialValue G (MIPRE.normalizedTrace (Fin S.d)) S.P

theorem MIPRE.SyncStrategy.value_eq {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : S.value = ∑ x : X, ∑ y : X, ∑ a : A, ∑ b : A, (G.μ x y * if G.D x y a b = true then 1 else 0) * ((S.P.M x a * S.P.M y b).trace.re / ↑S.d)

The value of a synchronous strategy, written out (the spelling of blueprint def:sync-value and of MIPRE.HaltingGameValue.strategyValue): the players answer questions (x, y) with (a, b) with probability Tr(M^x_a M^y_b)/d.

theorem MIPRE.SyncStrategy.value_nonneg {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : 0 ≤ S.value

The value of a synchronous strategy is nonnegative.

theorem MIPRE.SyncStrategy.value_le_one {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : S.value ≤ 1

The value of a synchronous strategy is at most one.

def MIPRE.SyncStrategy.povm {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (x : X) : POVM A (Fin S.d)

The measurements of a synchronous strategy, packaged as POVMs (positivity follows from projectivity). This is the interface to the QuantumLib-compatible POVM layer.

Equations

• S.povm x = { mats := fun (a : A) => ⟨S.P.M x a, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

def MIPRE.SyncStrategy.ofPOVM {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (d : ℕ) (d_pos : 0 < d) (povm : X → POVM A (Fin d)) (projective : ∀ (x : X) (a : A), ↑((povm x).mats a) * ↑((povm x).mats a) = ↑((povm x).mats a)) : SyncStrategy G

Build a synchronous strategy from POVM data with a projectivity certificate (the packaging of MIPRE.HaltingGameValue.SyncStrategy).

Equations

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

def MIPRE.SyncStrategy.IsPCC {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : Prop

A synchronous strategy is PCC (projective, consistent, and commuting, following JNVWY Section 5.2; blueprint def:pcc) if the measurement operators associated with any pair of questions asked with positive probability commute. Projectivity is part of SyncStrategy, and consistency is automatic for synchronous strategies (ProjectiveMeasurement.consistency), so only the commutation condition remains.

Equations

• S.IsPCC = ∀ (x y : X), 0 < G.μ x y → ∀ (a b : A), S.P.M x a * S.P.M y b = S.P.M y b * S.P.M x a

noncomputable def MIPRE.syncValue {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : ℝ

The synchronous value of a synchronous game (blueprint def:sync-value): the supremum of strategy values over all synchronous strategies.

Equations

• MIPRE.syncValue G = ⨆ (S : MIPRE.SyncStrategy G), S.value

Commuting strategies and the commuting value

structure MIPRE.CommutingStrategy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : Type (max (max 1 u_1) u_3)

A commuting strategy for a synchronous game (blueprint def:commuting-strategy): a unital C*-algebra alg with a tracial state τ, together with a question-indexed projective measurement family in alg. Outcome probabilities are computed with τ (see CommutingStrategy.value).

The algebra lives in universe 0; by the GNS representation this loses no generality (see the module docstring).

• alg : Type

  The underlying unital C*-algebra.

• cstarAlgebra : CStarAlgebra self.alg

  The C*-algebra structure.

• τ : TracialState self.alg

  The tracial state.

• P : ProjectiveMeasurement X A self.alg

  The measurements: for each question, a projective measurement in alg.

noncomputable def MIPRE.CommutingStrategy.value {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : CommutingStrategy G) : ℝ

The value of a commuting strategy in G (blueprint def:commuting-value): the generic tracial value; the players answer questions (x, y) with (a, b) with probability τ(M^x_a M^y_b).

Equations

• S.value = MIPRE.tracialValue G S.τ S.P

theorem MIPRE.CommutingStrategy.value_nonneg {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : CommutingStrategy G) : 0 ≤ S.value

The value of a commuting strategy is nonnegative.

theorem MIPRE.CommutingStrategy.value_le_one {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : CommutingStrategy G) : S.value ≤ 1

The value of a commuting strategy is at most one.

theorem MIPRE.CommutingStrategy.bddAbove_range_value {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : BddAbove (Set.range fun (S : CommutingStrategy G) => S.value)

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

noncomputable def MIPRE.commValue {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : ℝ

The commuting value of a synchronous game (blueprint def:commuting-value): the supremum of strategy values over all commuting strategies.

Equations

• MIPRE.commValue G = ⨆ (S : MIPRE.CommutingStrategy G), S.value

theorem MIPRE.commValue_nonneg {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : 0 ≤ commValue G

The commuting value is nonnegative.

A synchronous strategy is a commuting strategy

noncomputable def MIPRE.SyncStrategy.toCommutingStrategy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : CommutingStrategy G

A synchronous strategy is a commuting strategy (the content of blueprint lem:sync-le-valco): take the algebra of d × d complex matrices with the normalized trace. The algebra is realized as CStarMatrix (Fin d) (Fin d) ℂ — mathlib's type synonym of Matrix carrying the operator-norm CStarAlgebra instance — and the measurements and the state are transported along the definitionally trivial star-algebra equivalence CStarMatrix.ofMatrixStarAlgEquiv. The value is preserved: SyncStrategy.value_toCommutingStrategy.

Equations

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

@[simp]

theorem MIPRE.SyncStrategy.value_toCommutingStrategy {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) : S.toCommutingStrategy.value = S.value

SyncStrategy.toCommutingStrategy preserves the value — definitionally.

Entanglement requirement

noncomputable def MIPRE.entRequirement {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (ν : ℝ) : ℕ∞

The entanglement requirement Ent(G, ν) (blueprint def:ent): the least d such that there exists a synchronous strategy with dimension at most d achieving value at least ν in G, and ∞ if no synchronous strategy achieves ν. It is realized as the infimum in ℕ∞ of the dimensions of the achieving strategies, which takes the value ⊤ = ∞ when there are none.

Equations

• MIPRE.entRequirement G ν = ⨅ (S : { S : MIPRE.SyncStrategy G // ν ≤ S.value }), ↑(↑S).d

Relationship lemmas

theorem MIPRE.syncValue_le_quantumValue {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : syncValue G ≤ quantumValue G.toGame

The synchronous value lower-bounds the quantum value (blueprint lem:sync-le-valstar): a synchronous strategy {M^x_a} on ℂ^d yields the tensor-product strategy A^x_a = M^x_a, B^y_b = (M^y_b)ᵀ, ψ = d^{-1/2} ∑ᵢ |i⟩|i⟩ with the same value.

theorem MIPRE.syncValue_le_commValue {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : syncValue G ≤ commValue G

The synchronous value lower-bounds the commuting value (blueprint lem:sync-le-valco): a synchronous strategy on ℂ^d is a commuting strategy with alg = ℂ^{d × d} and τ = Tr/d (SyncStrategy.toCommutingStrategy), with the same value.