Tracial strategies as projective strategies in finite pairs

Phase 6 of planning/mipco-track.md (reports/lidt-co-audit.md, §3.4): below ω_co(G), and above 0, lies the value of a projective strategy for G in a dyadic pair (MIPRE.CommutingFinitePairApprox, lem:co-value-finite-pair). This file gives the steps that hold for every tracial strategy, which land in finite pairs; the theorem itself, MIPRE.Repetition.commutingFinitePairApprox (MIPRE/Background/Repetition/DyadicApprox.lean), first amplifies the strategy so that its finite pair is dyadic (MIPRE/Background/Repetition/Amplify.lean). The analytic content is Lin's tracial density, in the form proved by the vendored development:

1. Strict tracial reduction. ω_co(G) is the commuting-operator value of the vendored development (MIPRE.Repetition.commutingOperatorValue_eq_omegaCO), and below it lies the winning probability of a tracially embeddable strategy T (CommutingRepetition.strict_tracial_reduction): a tracial algebra in standard form L²(𝒜, τ), a density σ, the first player's POVMs acting on the left and the second player's on the right, in the state ι σ.
2. The standard-form pair. On L²(𝒜, τ), the commutant of the right action (StdTracialAlgebra.vnAlg) and its commutant are a finite pair (isFinitePair_stdModel): the trace vector ι 1 is tracial on the first (StdTracialAlgebra.traceState_mul_comm_vn) and, through the conjugation J, on the second, and it separates both, being cyclic for the left and for the right actions. The left action lies in the first, the right action in the second, so T is a POVM strategy of this model, of value its winning probability (povmValue_stdModel, through BipartiteModel.value_toCommuting and TracialStrategy.toCommutingStrategy_correlation).
3. Projectivity (exists_projStrat_expand_stdModel). Each player's POVMs dilate to projective measurements in the matrices over the player's algebra against one fixed basis vector (MIPRE.exists_pvm_dilation); in the ancilla extension at that basis vector they form a projective strategy of the same value (BipartiteModel.povmValue_expand_basisVec), and the extension is a finite pair (BipartiteModel.IsFinitePair.expand), or a dyadic pair if the standard-form model is one (BipartiteModel.IsDyadicPair.expand).

An empty answer alphabet leaves no strategy, so ω_co(G) = 0, below every admissible threshold; a game's question sets are nonempty, its distribution summing to 1 (nonempty_of_lt_commutingOperatorValue). Otherwise the alphabets are those of the vendored theorem, which assumes them nonempty.

The standard-form pair

noncomputable def MIPRE.Repetition.rightVN (M : CommutingRepetition.StdTracialAlgebra) : StarSubalgebra ℂ (M.H →L[ℂ] M.H)

The commutant of StdTracialAlgebra.vnAlg: the von Neumann algebra R(𝒜)'' generated by the right action, in which the second player's operators lie.

Equations

• MIPRE.Repetition.rightVN M = StarSubalgebra.centralizer ℂ ↑M.vnAlg

instance MIPRE.Repetition.instStarOrderedRingSubtypeContinuousLinearMapComplexIdHMemStarSubalgebraVnAlg (M : CommutingRepetition.StdTracialAlgebra) : StarOrderedRing ↥M.vnAlg

R(𝒜)' carries the operator order, as a commutant.

instance MIPRE.Repetition.instStarOrderedRingSubtypeContinuousLinearMapComplexIdHMemStarSubalgebraRightVN (M : CommutingRepetition.StdTracialAlgebra) : StarOrderedRing ↥(rightVN M)

R(𝒜)'' carries the operator order, as a commutant.

theorem MIPRE.Repetition.mem_rightVN_iff {M : CommutingRepetition.StdTracialAlgebra} {y : M.H →L[ℂ] M.H} : y ∈ rightVN M ↔ ∀ g ∈ M.vnAlg, g * y = y * g

R(𝒜)'' is the set of operators commuting with R(𝒜)', which is closed under adjoints.

theorem MIPRE.Repetition.Rop_mem_rightVN (M : CommutingRepetition.StdTracialAlgebra) (a : M.A) : M.Rop a ∈ rightVN M

The right action lies in R(𝒜)''.

theorem MIPRE.Repetition.L_mul_eq_of_mem_rightVN (M : CommutingRepetition.StdTracialAlgebra) {y : M.H →L[ℂ] M.H} (hy : y ∈ rightVN M) (a : M.A) : M.L a * y = y * M.L a

The left action commutes with R(𝒜)''.

theorem MIPRE.Repetition.L_traceVector (M : CommutingRepetition.StdTracialAlgebra) (a : M.A) : (M.L a) M.traceVector = M.ι a

The left action on the trace vector is the embedding ι of 𝒜 into L²(𝒜, τ).

theorem MIPRE.Repetition.eq_zero_of_mem_vnAlg (M : CommutingRepetition.StdTracialAlgebra) {x : M.H →L[ℂ] M.H} (hx : x ∈ M.vnAlg) (h0 : x M.traceVector = 0) : x = 0

The trace vector separates R(𝒜)', being cyclic for the right action.

theorem MIPRE.Repetition.eq_zero_of_mem_rightVN (M : CommutingRepetition.StdTracialAlgebra) {y : M.H →L[ℂ] M.H} (hy : y ∈ rightVN M) (h0 : y M.traceVector = 0) : y = 0

The trace vector separates R(𝒜)'', being cyclic for the left action.

theorem MIPRE.Repetition.traceState_conjJ_eq (M : CommutingRepetition.StdTracialAlgebra) (G : M.H →L[ℂ] M.H) : M.traceState (M.conjJ G) = star (M.traceState G)

The trace-vector state of J G J is the conjugate of that of G.

theorem MIPRE.Repetition.traceState_mul_comm_rightVN (M : CommutingRepetition.StdTracialAlgebra) {y y' : M.H →L[ℂ] M.H} (hy : y ∈ rightVN M) (hy' : y' ∈ rightVN M) : M.traceState (y * y') = M.traceState (y' * y)

The trace-vector state is tracial on R(𝒜)'': conjugation by J carries R(𝒜)'' into R(𝒜)', where it is (StdTracialAlgebra.traceState_mul_comm_vn).

noncomputable def MIPRE.Repetition.stdModel (M : CommutingRepetition.StdTracialAlgebra) (ψ : M.H) : BipartiteModel (M.H →L[ℂ] M.H) ↥M.vnAlg ↥(rightVN M)

The standard-form model of a tracial algebra in a state ψ of L²(𝒜, τ): the operators of L²(𝒜, τ) represented on it, the commutant R(𝒜)' of the right action as the first player's algebra and its commutant R(𝒜)'' as the second player's.

Equations

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

theorem MIPRE.Repetition.mem_opsA_stdModel {M : CommutingRepetition.StdTracialAlgebra} {ψ : M.H} {T : M.H →L[ℂ] M.H} : T ∈ (stdModel M ψ).opsA ↔ T ∈ M.vnAlg

The first player's operators of the standard-form model are R(𝒜)'.

theorem MIPRE.Repetition.mem_opsB_stdModel {M : CommutingRepetition.StdTracialAlgebra} {ψ : M.H} {T : M.H →L[ℂ] M.H} : T ∈ (stdModel M ψ).opsB ↔ T ∈ rightVN M

The second player's operators of the standard-form model are R(𝒜)''.

theorem MIPRE.Repetition.isFinitePair_stdModel (M : CommutingRepetition.StdTracialAlgebra) (ψ : M.H) : (stdModel M ψ).IsFinitePair

The standard-form model is a finite pair, with the trace vector as the faithful tracial state of both players' algebras.

A tracial strategy in its standard-form model

noncomputable def MIPRE.Repetition.measA {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : CommutingRepetition.TracialStrategy X Y A B) (x : X) : POVMIn A ↥T.M.vnAlg

The first player's measurement of a tracial strategy at a question: the left action of its POVM, in R(𝒜)'.

Equations

• MIPRE.Repetition.measA T x = { mats := fun (a : A) => ⟨⟨T.M.L (T.E x a), ⋯⟩, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

noncomputable def MIPRE.Repetition.measB {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : CommutingRepetition.TracialStrategy X Y A B) (y : Y) : POVMIn B ↥(rightVN T.M)

The second player's measurement of a tracial strategy at a question: the right action of its POVM, in R(𝒜)''.

Equations

• MIPRE.Repetition.measB T y = { mats := fun (b : B) => ⟨⟨T.M.Rop (T.F y b), ⋯⟩, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

theorem MIPRE.Repetition.povmValue_stdModel {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (T : CommutingRepetition.TracialStrategy X Y A B) (G : Game X Y A B) : (stdModel T.M (T.M.ι T.σ)).povmValue G (measA T) (measB T) = (toCR G).win T.correlation

A tracial strategy is a POVM strategy of its standard-form model, in the state ι σ, of value its winning probability.

theorem MIPRE.Repetition.nonempty_of_lt_commutingOperatorValue {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {t : ℝ} (ht : 0 ≤ t) (h : t < commutingOperatorValue G) : Nonempty X ∧ Nonempty Y ∧ Nonempty A ∧ Nonempty B

The alphabets of a game of positive commuting-operator value are nonempty: a game's question sets are nonempty, its distribution summing to 1, and an empty answer alphabet leaves no strategy, so ω_co(G) = 0, below every admissible threshold.

theorem MIPRE.Repetition.exists_projStrat_expand_stdModel {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) (T : CommutingRepetition.TracialStrategy X Y A B) : ∃ (α : Type) (β : Type) (x : Fintype α) (x_1 : DecidableEq α) (x_2 : Fintype β) (x_3 : DecidableEq β) (_ : Nonempty α) (_ : Nonempty β) (e : α × β → ℂ) (S : ((stdModel T.M (T.M.ι T.σ)).expand e).ProjStrat G), S.value = (toCR G).win T.correlation

A tracial strategy is a projective strategy of an ancilla extension of its standard-form model, of value its winning probability: each player's POVMs dilate to projective measurements in the matrices over the player's algebra against one fixed basis vector (exists_pvm_dilation), and in the extension at that basis vector they have the value of the POVMs (BipartiteModel.povmValue_expand_basisVec, povmValue_stdModel). The registers are nonempty, so the extension is a finite pair, or a dyadic pair, when the standard-form model is one.