Amplification by an algebra with dyadic matrix units

The orthonormalization step of the C6b port applies in dyadic pairs (BipartiteModel.IsDyadicPair, MIPRE/Foundations/DyadicPair.lean), and the finite pairs that commutingFinitePairApprox builds are the ancilla extensions of standard-form models stdModel M ψ of tracial algebras M, which need not have any matrix units. This file tensors them with a fixed tracial algebra B that has unital dyadic matrix units, at no cost in value (reports/c6b-paper-proofs.md, §3, Theorems A and T).

• The standard-form pair of M ⊗ B is dyadic (isDyadicPair_stdModel_tensorStep, Theorem A): the units 1 ⊗ fᵢⱼ of M ⊗ B act on the left in R(M ⊗ B)' and, through the opposite algebra, on the right in R(M ⊗ B)''. So are its ancilla extensions with nonempty registers (BipartiteModel.IsDyadicPair.expand), whence both hypotheses hII of the orthonormalization step.
• Amplification (amplify, Theorem T): a tracial strategy (σ, E, F) in M gives the tracial strategy (σ ⊗ 1, E ⊗ 1, F ⊗ 1) in M ⊗ B, of the same correlation (amplify_correlation), the trace of M ⊗ B restricting to that of M on M ⊗ 1.
• The value consequence (exists_tracialStrategy_isDyadicPair): strict tracial reduction with a strategy whose standard-form model is dyadic in every state, which is what commutingFinitePairApprox needs to land in dyadic pairs.

The standard-form pair of an amplified algebra

noncomputable def MIPRE.Repetition.leftVNHom (M : CommutingRepetition.StdTracialAlgebra) : M.A →⋆ₐ[ℂ] ↥M.vnAlg

The left action as a ∗-homomorphism into R(𝒜)': StdTracialAlgebra.L, corestricted to the first player's algebra of the standard-form model.

Equations

• MIPRE.Repetition.leftVNHom M = M.L.codRestrict M.vnAlg ⋯

noncomputable def MIPRE.Repetition.rightVNHom (M : CommutingRepetition.StdTracialAlgebra) : M.Aᵐᵒᵖ →⋆ₐ[ℂ] ↥(rightVN M)

The right action as a ∗-homomorphism into R(𝒜)'': StdTracialAlgebra.R, on the opposite algebra, corestricted to the second player's algebra of the standard-form model.

Equations

• MIPRE.Repetition.rightVNHom M = M.R.codRestrict (MIPRE.Repetition.rightVN M) ⋯

theorem MIPRE.Repetition.isDyadicPair_stdModel (M : CommutingRepetition.StdTracialAlgebra) (hM : HasDyadicUnits M.A) (ψ : M.H) : (stdModel M ψ).IsDyadicPair

The standard-form model of a tracial algebra with unital dyadic matrix units is a dyadic pair (lem:amplification-dyadic, item A), in every state: the units act on the left in R(𝒜)' and, through the opposite algebra, on the right in R(𝒜)''.

theorem MIPRE.Repetition.hasDyadicUnits_tensorStep (M B : CommutingRepetition.StdTracialAlgebra) (hB : HasDyadicUnits B.A) : HasDyadicUnits (M.tensorStep B).A

M ⊗ B has unital dyadic matrix units when B has (lem:amplification-dyadic, item A): the units 1 ⊗ fᵢⱼ.

theorem MIPRE.Repetition.isDyadicPair_stdModel_tensorStep (M B : CommutingRepetition.StdTracialAlgebra) (hB : HasDyadicUnits B.A) (ψ : (M.tensorStep B).H) : (stdModel (M.tensorStep B) ψ).IsDyadicPair

The standard-form pair of M ⊗ B is a dyadic pair (lem:amplification-dyadic, item A; Theorem A of reports/c6b-paper-proofs.md, §3) when B has unital dyadic matrix units, in every state.

noncomputable def MIPRE.Repetition.inclLeft (M B : CommutingRepetition.StdTracialAlgebra) : M.A →⋆ₐ[ℂ] (M.tensorStep B).A

The embedding a ↦ a ⊗ 1 of M into M ⊗ B: StdTracialAlgebra.stepInclLeft, typed into the carrier of tensorStep M B, so that its images carry that algebra's instances.

Equations

• MIPRE.Repetition.inclLeft M B = M.stepInclLeft B

theorem MIPRE.Repetition.τ_inclLeft (M B : CommutingRepetition.StdTracialAlgebra) (a : M.A) : (M.tensorStep B).τ ((inclLeft M B) a) = M.τ a

The trace of M ⊗ B restricts to that of M on M ⊗ 1.

Amplification of a tracial strategy

theorem MIPRE.Repetition.isPosElem_map {R : Type u_1} {S : Type u_2} {F : Type u_3} [NonUnitalNonAssocSemiring R] [StarRing R] [NonUnitalNonAssocSemiring S] [StarRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] [StarHomClass F R S] (φ : F) {a : R} (h : CommutingRepetition.IsPosElem a) : CommutingRepetition.IsPosElem (φ a)

A ∗-homomorphism maps positive elements to positive elements: it carries a sum of squares ∑ cᵢ⋆ cᵢ to the sum of squares of the images. Unlike IsPosElem.starAlgHom_map, it asks for no StarModule instance, which instance search does not find on the carrier of tensorStep.

noncomputable def MIPRE.Repetition.amplify {X Y A' B' : Type} [Fintype X] [Fintype Y] [Fintype A'] [Fintype B'] (T : CommutingRepetition.TracialStrategy X Y A' B') (B : CommutingRepetition.StdTracialAlgebra) : CommutingRepetition.TracialStrategy X Y A' B'

The amplified strategy (lem:amplification-dyadic, item T; Theorem T of reports/c6b-paper-proofs.md, §3): the density σ ⊗ 1 and the measurements E ⊗ 1 and F ⊗ 1 in M ⊗ B, for a tracial strategy (σ, E, F) in M.

Equations

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

theorem MIPRE.Repetition.amplify_correlation {X Y A' B' : Type} [Fintype X] [Fintype Y] [Fintype A'] [Fintype B'] (T : CommutingRepetition.TracialStrategy X Y A' B') (B : CommutingRepetition.StdTracialAlgebra) : (amplify T B).correlation = T.correlation

The amplified strategy has the same correlation (lem:amplification-dyadic, item T), the trace of M ⊗ B restricting to that of M on M ⊗ 1.

theorem MIPRE.Repetition.isDyadicPair_stdModel_amplify {X Y A' B' : Type} [Fintype X] [Fintype Y] [Fintype A'] [Fintype B'] (T : CommutingRepetition.TracialStrategy X Y A' B') (B : CommutingRepetition.StdTracialAlgebra) (hB : HasDyadicUnits B.A) (ψ : (amplify T B).M.H) : (stdModel (amplify T B).M ψ).IsDyadicPair

The standard-form model of an amplified strategy is a dyadic pair (lem:amplification-dyadic), in every state, when B has unital dyadic matrix units.

theorem MIPRE.Repetition.exists_tracialStrategy_isDyadicPair {X Y A' B' : Type} [Fintype X] [Fintype Y] [Fintype A'] [Fintype B'] [Nonempty X] [Nonempty Y] [Nonempty A'] [Nonempty B'] (B : CommutingRepetition.StdTracialAlgebra) (hB : HasDyadicUnits B.A) (H : CommutingRepetition.Game X Y A' B') {lam : ℝ} (hlam : lam < H.omegaCO) : ∃ (T : CommutingRepetition.TracialStrategy X Y A' B'), lam < H.win T.correlation ∧ ∀ (ψ : T.M.H), (stdModel T.M ψ).IsDyadicPair

Strict tracial reduction into dyadic pairs (lem:amplification-dyadic, its consequence): below ω_co(H) lies the winning probability of a tracial strategy whose standard-form model is a dyadic pair in every state, given one tracial algebra B with unital dyadic matrix units. It is CommutingRepetition.strict_tracial_reduction followed by amplification by B, which keeps the correlation (amplify_correlation).