Tracial strategies are commuting-operator strategies

Blueprint lem:tracial-le-co: for every synchronous game G, the tracial commuting value is at most the bipartite commuting-operator value, commValue G ≤ commutingOperatorValue G.toGame.

Given a commuting strategy (𝒜, τ, M), the GNS space of τ (MIPRE/Foundations/GNS.lean) is the completion of 𝒜 for ⟨a, b⟩ = τ(a⋆ b), with the class of 1 as the unit vector. The first player's operators are the lifts of left multiplication by M^x_a, the second player's those of right multiplication by M^y_b. Left and right multiplications commute exactly, by associativity, and the correlation is τ(1⋆ M^x_a M^y_b) = τ(M^x_a M^y_b), so the strategy has the value of (𝒜, τ, M).

Right multiplication by a projection g is where the trace is used. It is a contraction, τ((s g)⋆ (s g)) = τ(s⋆ s g) ≤ τ(s⋆ s) because τ(s⋆ s (1 - g)) = τ((s (1 - g))⋆ (s (1 - g))). It is symmetric for the form, τ((s g)⋆ t) = τ(s⋆ t g), and positive, τ(s⋆ s g) = τ((s g)⋆ (s g)). No norm on 𝒜 is used: the argument is algebraic in the projections and the trace, and the bounds come from the positivity of τ alone.

A tracial state is Hermitian, τ(a⋆) = conj τ(a), by polarization of its positivity at 1 + a and 1 + i a (TracialState.map_star). So it is a GNS state (TracialState.toState).

Main declarations

• TracialState.map_star, TracialState.toState;
• TracialCo.bdd_mulRight, TracialCo.lift_mulRight_isPositive;
• CommutingStrategy.toCommutingOperatorStrategy, CommutingStrategy.value_toCommutingOperator;
• commValue_le_commutingOperatorValue.

theorem MIPRE.TracialState.im_star_mul_self {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (τ : TracialState 𝒜) (m : 𝒜) : (τ (star m * m)).im = 0

The value of a tracial state on m⋆ m is real.

theorem MIPRE.TracialState.map_star {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) (a : 𝒜) : τ (star a) = (starRingEnd ℂ) (τ a)

A tracial state is Hermitian: τ(a⋆) = conj τ(a), by polarization of positivity at 1 + a and 1 + i a.

def MIPRE.TracialState.toState {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) : GNS.State 𝒜

A tracial state as a GNS state (MIPRE.GNS.State).

Equations

• τ.toState = { L := τ.toLinearMap, map_one := ⋯, map_star := ⋯, nonneg := ⋯ }

@[simp]

theorem MIPRE.TracialState.toState_L {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) (a : 𝒜) : τ.toState.L a = τ a

theorem MIPRE.TracialCo.form_mulRight_left {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (τ : TracialState 𝒜) {g : 𝒜} (hgs : star g = g) (s t : 𝒜) : τ (star (s * g) * t) = τ (star s * (t * g))

The GNS form of τ against right multiplication: τ((s g)⋆ t) = τ(s⋆ t g) for self-adjoint g.

theorem MIPRE.TracialCo.form_mulRight_self {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (τ : TracialState 𝒜) {g : 𝒜} (hgs : star g = g) (hgg : g * g = g) (s : 𝒜) : τ (star s * (s * g)) = τ (star (s * g) * (s * g))

For a projection g, τ(s⋆ s g) = τ((s g)⋆ (s g)).

theorem MIPRE.TracialCo.bdd_mulRight {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) {g : 𝒜} (hgs : star g = g) (hgg : g * g = g) : GNS.Bdd τ.toState.form (LinearMap.mulRight ℂ g)

Right multiplication by a projection is a contraction for the GNS form of a tracial state.

theorem MIPRE.TracialCo.lift_mulRight_isPositive {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) {g : 𝒜} (hgs : star g = g) (hgg : g * g = g) : (GNS.lift τ.toState.form (LinearMap.mulRight ℂ g) ⋯).IsPositive

The lift of right multiplication by a projection is a positive operator.

theorem MIPRE.TracialCo.bdd_mulLeft {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) {g : 𝒜} (hgs : star g = g) (hgg : g * g = g) : GNS.Bdd τ.toState.form (LinearMap.mulLeft ℂ g)

Left multiplication by a projection is bounded for the GNS form of a tracial state.

theorem MIPRE.TracialCo.lift_mulLeft_isPositive {𝒜 : Type} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (τ : TracialState 𝒜) {g : 𝒜} (hgs : star g = g) (hgg : g * g = g) : (GNS.lift τ.toState.form (LinearMap.mulLeft ℂ g) ⋯).IsPositive

The lift of left multiplication by a projection is a positive operator.

The commuting-operator strategy of a commuting strategy

noncomputable def MIPRE.CommutingStrategy.toCommutingOperatorStrategy {X A : Type} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : CommutingStrategy G) : CommutingOperatorStrategy X X A A

The GNS strategy of a tracial strategy: on the GNS space of τ, with the cyclic vector ι 1, the first player multiplies on the left by M^x_a, the second on the right by M^y_b.

Equations

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

theorem MIPRE.CommutingStrategy.correlation_toCommutingOperatorStrategy {X A : Type} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : CommutingStrategy G) (x y : X) (a b : A) : S.toCommutingOperatorStrategy.correlation x y a b = (S.τ (S.P.M x a * S.P.M y b)).re

The correlation of the GNS strategy is Re τ(M^x_a M^y_b).

theorem MIPRE.CommutingStrategy.value_toCommutingOperatorStrategy {X A : Type} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : CommutingStrategy G) : CommutingOperatorStrategy.value G.toGame S.toCommutingOperatorStrategy = S.value

The GNS strategy has the value of the tracial strategy.

theorem MIPRE.commValue_le_commutingOperatorValue {X A : Type} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) : commValue G ≤ commutingOperatorValue G.toGame

Tracial strategies are commuting-operator strategies (blueprint lem:tracial-le-co): the commuting value of a synchronous game is at most the commuting-operator value of its bipartite game.