Role-register algebraic identities for the low individual degree test

Role-pair projection algebra, symmetrized measurement definitions, and expectation identities for the classical role-register symmetrized state.

Role-pair projection algebra

noncomputable def MIPStarRE.LDT.roleSymmetrizedMeasurement {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (MA MB : Measurement Outcome ι) : Measurement Outcome (Role × ι)

Block-diagonal role-register measurement built from an Alice-block and a Bob-block POVM.

This is the measurement-level analogue of symmetrizedIdxProjMeas: the Role.A sector carries MA, and the Role.B sector carries MB.

Equations

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

@[simp]

theorem MIPStarRE.LDT.roleSymmetrizedMeasurement_outcome {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (MA MB : Measurement Outcome ι) (a : Outcome) : (roleSymmetrizedMeasurement MA MB).outcome a = roleCond Role.A (MA.outcome a) + roleCond Role.B (MB.outcome a)

@[simp]

theorem MIPStarRE.LDT.roleSymmetrizedMeasurement_total {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (MA MB : Measurement Outcome ι) : (roleSymmetrizedMeasurement MA MB).total = 1

theorem MIPStarRE.LDT.qBipartiteConsDefect_of_measurements {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (A : Measurement Outcome ιA) (B : Measurement Outcome ιB) : qBipartiteConsDefect ψ A.toSubMeas B.toSubMeas = ev ψ 1 - qBipartiteMatchMass ψ A.toSubMeas B.toSubMeas

For complete measurements, the bipartite consistency defect is the total expectation minus the matching mass.

theorem MIPStarRE.LDT.opTensor_roleCond_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (XA XB YA YB : Quantum.Op ι) : opTensor (roleCond Role.A XA + roleCond Role.B XB) (roleCond Role.A YA + roleCond Role.B YB) = rolePairCond Role.A Role.A (opTensor XA YA) + rolePairCond Role.A Role.B (opTensor XA YB) + (rolePairCond Role.B Role.A (opTensor XB YA) + rolePairCond Role.B Role.B (opTensor XB YB))

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_rolePair_AB {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) (Z : Quantum.Op (ι × ι)) : ev (classicalRoleSymmState ψ) (rolePairCond Role.A Role.B Z) = 1 / 2 * ev ψ Z

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_rolePair_BA {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) (Z : Quantum.Op (ι × ι)) : ev (classicalRoleSymmState ψ) (rolePairCond Role.B Role.A Z) = 1 / 2 * ev (swapQuantumState ψ) Z

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_rolePair_AA {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) (Z : Quantum.Op (ι × ι)) : ev (classicalRoleSymmState ψ) (rolePairCond Role.A Role.A Z) = 0

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_rolePair_BB {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) (Z : Quantum.Op (ι × ι)) : ev (classicalRoleSymmState ψ) (rolePairCond Role.B Role.B Z) = 0

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_opTensor_roleCond_A {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) (X : Quantum.Op ι) (Y : Quantum.Op (Role × ι)) : ev (classicalRoleSymmState ψ) (opTensor (roleCond Role.A X) Y) = 1 / 2 * ev ψ (opTensor X (roleBlock Role.B Y))

theorem MIPStarRE.LDT.ev_classicalRoleSymmState_opTensor_roleCond_B {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (ψ : QuantumState (ι × ι)) (X : Quantum.Op ι) (Y : Quantum.Op (Role × ι)) : ev (classicalRoleSymmState ψ) (opTensor (roleCond Role.B X) Y) = 1 / 2 * ev ψ (opTensor (roleBlock Role.A Y) X)