Section 10 commutativity points: shared helpers core

Shared reindexing and tensor-placement helpers used by the Section 10 commutativity-of-points argument.

References

• references/ldt-paper/commutativity-points.tex
• blueprint/src/chapter/ch08_commutativity.tex

Shared reindexing and tensor-placement helpers

theorem MIPStarRE.LDT.CommutativityPoints.sddOpRel_symm {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) (δ : Error) : SDDOpRel ψ 𝒟 A B δ → SDDOpRel ψ 𝒟 B A δ

theorem MIPStarRE.LDT.CommutativityPoints.qSDDOp_reindex {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} {Outcome' : Type u_3} [Fintype Outcome] [Fintype Outcome'] (e : Outcome ≃ Outcome') (ψ : QuantumState ι) (A B : OpFamily Outcome ι) : qSDDOp ψ A B = qSDDOp ψ { outcome := fun (a' : Outcome') => A.outcome (e.symm a'), total := A.total } { outcome := fun (a' : Outcome') => B.outcome (e.symm a'), total := B.total }

Reindexing the outcome type of both operator families preserves qSDDOp.

theorem MIPStarRE.LDT.CommutativityPoints.sddOpRel_reindex {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} {Outcome' : Type u_4} [Fintype Outcome] [Fintype Outcome'] (e : Outcome ≃ Outcome') (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) (δ : Error) : SDDOpRel ψ 𝒟 A B δ → SDDOpRel ψ 𝒟 (fun (q : Question) => { outcome := fun (a' : Outcome') => (A q).outcome (e.symm a'), total := (A q).total }) (fun (q : Question) => { outcome := fun (a' : Outcome') => (B q).outcome (e.symm a'), total := (B q).total }) δ

Reindexing the outcome type of both indexed families preserves SDDOpRel.

theorem MIPStarRE.LDT.CommutativityPoints.sddOpRel_congr_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B A' B' : IdxOpFamily Question Outcome ι) (δ : Error) (hA : ∀ (q : Question) (a : Outcome), (A q).outcome a = (A' q).outcome a) (hB : ∀ (q : Question) (a : Outcome), (B q).outcome a = (B' q).outcome a) : SDDOpRel ψ 𝒟 A B δ → SDDOpRel ψ 𝒟 A' B' δ

Pointwise equality of outcomes preserves SDDOpRel.

theorem MIPStarRE.LDT.CommutativityPoints.subMeas_sum_adjoint_mul_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome ι) : ∑ a : Outcome, Matrix.conjTranspose (A.outcome a) * A.outcome a ≤ 1

theorem MIPStarRE.LDT.CommutativityPoints.liftLeft_mul_leftPlaced_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (a : α) (b : β) : A.liftLeft.outcome a * B.toOpFamily.leftPlacedOpFamily.outcome b = leftTensor (A.outcome a * B.outcome b)

Multiplying a left lift with a left-placed family stays on the left tensor factor.

theorem MIPStarRE.LDT.CommutativityPoints.liftLeft_mul_rightPlaced_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (a : α) (b : β) : A.liftLeft.outcome a * B.toOpFamily.rightPlacedOpFamily.outcome b = opTensor (A.outcome a) (B.outcome b)

Multiplying a left lift with a right-placed family gives the tensor product.

theorem MIPStarRE.LDT.CommutativityPoints.liftRight_mul_leftPlaced_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (a : α) (b : β) : A.liftRight.outcome a * B.toOpFamily.leftPlacedOpFamily.outcome b = opTensor (B.outcome b) (A.outcome a)

Multiplying a right lift with a left-placed family gives the tensor product.

theorem MIPStarRE.LDT.CommutativityPoints.liftRight_mul_rightPlaced_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (a : α) (b : β) : A.liftRight.outcome a * B.toOpFamily.rightPlacedOpFamily.outcome b = rightTensor (A.outcome a * B.outcome b)

Multiplying a right lift with a right-placed family stays on the right tensor factor.