The commutation analysis

Blueprint lem:commutation-analysis (the paper's, in games.tex), and the two facts it runs on. It is the step that turns consistency with a joint measurement on the other side into approximate commutation on one side, and it is the only place in the Pauli appendix where projectivity of a measurement is genuinely used.

The shape

Alice has two POVMs A_b and C_c; Bob has one projective measurement P_{b,c} whose outcome is the pair. If each of Alice's is cross-party close to the corresponding marginal of Bob's, then Alice's two commute on the state:

A_b (x) Id ~ Id (x) P_b   and   C_c (x) Id ~ Id (x) P_c    =>    [A_b, C_c] (x) Id ~ 0 .

The proof moves both products to the same operator on Bob's side, Id (x) P_{b,c}, and that is where projectivity enters: for a projective measurement with a product outcome set the two marginals commute and multiply to the joint element (IsPVM.marg_mul_marg). Nothing else about P is used.

What the steps need

Each step multiplies a known deviation by an operator in front. The fact that lets it is the paper's fact:add-a-proj: if sum_i F_i^dag F_i <= Id then sum_i ||F_i v||^2 <= ||v||^2, so putting a family in front of a deviation costs nothing and adds its index to the sum. For a POVM that hypothesis is A_b^2 <= A_b and sum_b A_b = Id, with no projectivity (sum_aOp_conjTranspose_mul_self_le_one).

The constant is 16 delta: each side of the commutator reaches Id (x) P_{b,c} in two steps (4 delta after one triangle inequality), and the commutator is one more triangle (2 * 4 + 2 * 4). No square root anywhere.

In a model

The steps are proved for a state model (StateModel), with the families in its algebra and the hypothesis sum_i F_i^dag F_i <= Id on the represented operators (StateModel.IsColContraction); the analysis for a bipartite model (BipartiteModel.commutation_analysis), two POVMs in the first player's algebra against a projective measurement in the second player's. The matrix statements are their instances in the matrix and tensor-product models.

The steps in a state model

theorem MIPRE.StateModel.isColContraction_of_isPVMIn {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_2} [Fintype ι] {Q : ι → 𝒞} (h : IsPVMIn Q) : M.IsColContraction Q

A projective measurement is a column contraction, with equality.

theorem MIPRE.StateModel.snorm_sq_sum_proj_mul {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_2} [DecidableEq ι] {P : ι → 𝒞} (hPsa : ∀ (i : ι), star (P i) = P i) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) (W : ι → 𝒞) (s : Finset ι) : M.snorm (∑ i ∈ s, P i * W i) ^ 2 = ∑ i ∈ s, M.snorm (P i * W i) ^ 2

A sum of mutually orthogonal projections times arbitrary operators has orthogonal terms. The cross terms carry P i * P j = 0, so the squared state norm is additive --- exactly, and with no appeal to the size of the index set.

theorem MIPRE.StateModel.sum_snorm_sq_cool {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {A : ι → 𝒞} (hA : IsPVMIn A) (B : ι → 𝒞) (f : ι → κ) : ∑ k : κ, M.snorm (∑ i : ι with f i = k, (A i - A i * B i)) ^ 2 ≤ ∑ i : ι, M.snorm (A i - B i) ^ 2

lem:cool-closeness-fact, in its partition form. A projective measurement A that is δ-close to a family B stays δ-close to it after multiplying each element by A's own element and summing over the fibres of an outcome map, simultaneously over all the fibres: projectivity kills the cross terms inside a fibre (snorm_sq_sum_proj_mul), and each A i is a contraction.

theorem MIPRE.StateModel.sum_weighted_snorm_sq_triangle3 {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {ι : Type u_2} {κ : Type u_3} [Fintype κ] {w : ι → ℝ} (hw : ∀ (i : ι), 0 ≤ w i) (S : Finset ι) (P Q R T : ι → κ → 𝒞) : ∑ i ∈ S, w i * ∑ o : κ, M.snorm (P i o - T i o) ^ 2 ≤ 3 * ∑ i ∈ S, w i * ∑ o : κ, M.snorm (P i o - Q i o) ^ 2 + 3 * ∑ i ∈ S, w i * ∑ o : κ, M.snorm (Q i o - R i o) ^ 2 + 3 * ∑ i ∈ S, w i * ∑ o : κ, M.snorm (R i o - T i o) ^ 2

The weighted three-term triangle inequality, over a set of questions: the shape every item of lem:qld-win is stated in.

theorem MIPRE.StateModel.sum_prod_snorm_sq_mul_le_fst {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {B : Type u_2} {C : Type u_3} [Fintype B] [Fintype C] (F : B → 𝒞) (hF : M.IsColContraction F) (T : C → 𝒞) : ∑ p : B × C, M.snorm (F p.1 * T p.2) ^ 2 ≤ ∑ c : C, M.snorm (T c) ^ 2

Putting a family in front, with the front index in the first component of the pair.

theorem MIPRE.StateModel.sum_prod_snorm_sq_mul_le_snd {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {B : Type u_2} {C : Type u_3} [Fintype B] [Fintype C] (F : C → 𝒞) (hF : M.IsColContraction F) (T : B → 𝒞) : ∑ p : B × C, M.snorm (F p.2 * T p.1) ^ 2 ≤ ∑ b : B, M.snorm (T b) ^ 2

Putting a family in front, with the front index in the second component.

theorem MIPRE.StateModel.commutation_analysis_abstract {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {B : Type u_2} {C : Type u_3} [Fintype B] [Fintype C] {δ : ℝ} (alpha : B → 𝒞) (gamma : C → 𝒞) (betaB : B → 𝒞) (betaC : C → 𝒞) (betaBC : B × C → 𝒞) (halpha : M.IsColContraction alpha) (hgamma : M.IsColContraction gamma) (hbetaB : M.IsColContraction betaB) (hbetaC : M.IsColContraction betaC) (hcomm : ∀ (b : B) (c : C), alpha b * betaC c = betaC c * alpha b) (hcomm' : ∀ (b : B) (c : C), gamma c * betaB b = betaB b * gamma c) (hmul : ∀ (b : B) (c : C), betaC c * betaB b = betaBC (b, c)) (hmul' : ∀ (b : B) (c : C), betaB b * betaC c = betaBC (b, c)) (hA : ∑ b : B, M.snorm (alpha b - betaB b) ^ 2 ≤ δ) (hC : ∑ c : C, M.snorm (gamma c - betaC c) ^ 2 ≤ δ) : ∑ p : B × C, M.snorm (alpha p.1 * gamma p.2 - gamma p.2 * alpha p.1) ^ 2 ≤ 16 * δ

The commutation analysis, in one algebra. alpha and gamma are the two families that are to commute; betaB, betaC are what they are respectively close to, and betaBC is the joint operator both products reach.

The analysis in a bipartite model

theorem MIPRE.BipartiteModel.sum_xSqNorm_le_of_two_step {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {κ : Type u_4} [Fintype κ] (Q Q' : κ → 𝒜) (R : κ → ℬ) {a b : ℝ} (h1 : ∑ o : κ, M.stateSqNorm (Q o - Q' o) ≤ a) (h2 : ∑ o : κ, M.xSqNorm (Q' o) (R o) ≤ b) : ∑ o : κ, M.xSqNorm (Q o) (R o) ≤ 2 * a + 2 * b

Replacing the first player's operator by a nearby one on its own side, inside a cross-party deviation: one triangle inequality, at the usual cost of a factor two.

theorem MIPRE.BipartiteModel.isColContraction_πA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ι : Type u_4} [Fintype ι] (P : POVMIn ι 𝒜) : M.IsColContraction fun (i : ι) => M.πA (P.op i)

A POVM of the first player is a column contraction on the Hilbert space: t² ≤ t for each element, on the represented operator, and the elements sum to one. No projectivity.

theorem MIPRE.BipartiteModel.commutation_analysis {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {B : Type u_4} {C : Type u_5} [Fintype B] [Fintype C] {A : POVMIn B 𝒜} {Cm : POVMIn C 𝒜} {P : B × C → ℬ} (hP : IsPVMIn P) {δ : ℝ} (hA : ∑ b : B, M.xSqNorm (A.op b) (∑ c : C, P (b, c)) ≤ δ) (hC : ∑ c : C, M.xSqNorm (Cm.op c) (∑ b : B, P (b, c)) ≤ δ) : ∑ p : B × C, M.stateSqNorm (A.op p.1 * Cm.op p.2 - Cm.op p.2 * A.op p.1) ≤ 16 * δ

The commutation analysis (lem:commutation-analysis) in a bipartite model: two POVMs of the first player, each cross-party close to the corresponding marginal of one projective measurement of the second player, commute on the state at 16 δ.

The quadratic form is monotone

theorem MIPRE.qform_nonneg_of_nonneg {N : Type u_1} [Fintype N] [DecidableEq N] (v : N → ℂ) {Z : Matrix N N ℂ} (hZ : 0 ≤ Z) : 0 ≤ qform v Z

theorem MIPRE.qform_le_of_le {N : Type u_1} [Fintype N] [DecidableEq N] (v : N → ℂ) {X Y : Matrix N N ℂ} (h : X ≤ Y) : qform v X ≤ qform v Y

Adding an operator in front

fact:add-a-proj. Stated on the norm rather than on a distance, because that is the form both uses need: the family in front contributes its own index to the sum, and the deviation it is applied to does not change.

theorem MIPRE.sum_snorm_sq_mul_le {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} [Fintype ι] (v : N → ℂ) (F : ι → Matrix N N ℂ) (hF : ∑ i : ι, (F i).conjTranspose * F i ≤ 1) (M : Matrix N N ℂ) : ∑ i : ι, snorm v (F i * M) ^ 2 ≤ snorm v M ^ 2

A family of operators with sum_i F_i^dag F_i <= Id costs nothing in front.

theorem MIPRE.snorm_sq_mul_le_of_contraction {N : Type u_1} [Fintype N] [DecidableEq N] (v : N → ℂ) {P : Matrix N N ℂ} (hP : P.conjTranspose * P ≤ 1) (M : Matrix N N ℂ) : snorm v (P * M) ^ 2 ≤ snorm v M ^ 2

A contraction in front costs nothing. The one-operator case of sum_snorm_sq_mul_le.

theorem MIPRE.snorm_sq_sum_proj_mul {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (v : N → ℂ) {P : ι → Matrix N N ℂ} (hPsa : ∀ (i : ι), (P i).conjTranspose = P i) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) (W : ι → Matrix N N ℂ) (s : Finset ι) : snorm v (∑ i ∈ s, P i * W i) ^ 2 = ∑ i ∈ s, snorm v (P i * W i) ^ 2

A sum of mutually orthogonal projections times arbitrary operators has orthogonal terms. The cross terms carry P i * P j = 0, so the squared state norm is additive --- exactly, and with no appeal to the size of the index set.

theorem MIPRE.sum_snorm_sq_cool {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (v : N → ℂ) {A : ι → Matrix N N ℂ} (hA : IsPVM A) (B : ι → Matrix N N ℂ) (f : ι → κ) : ∑ k : κ, snorm v (∑ i : ι with f i = k, (A i - A i * B i)) ^ 2 ≤ ∑ i : ι, snorm v (A i - B i) ^ 2

lem:cool-closeness-fact, in its partition form. A projective measurement A that is delta-close to a family B stays delta-close to it after multiplying each element by A's own element and summing over the fibres of an outcome map --- simultaneously over all the fibres, which is what the consumers need: the single-subset form applied to the q fibres of an outcome map one at a time would cost a factor q.

theorem MIPRE.sum_snorm_sq_triangle' {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} [Fintype ι] (v : N → ℂ) (P Q R : ι → Matrix N N ℂ) : ∑ i : ι, snorm v (P i - R i) ^ 2 ≤ 2 * ∑ i : ι, snorm v (P i - Q i) ^ 2 + 2 * ∑ i : ι, snorm v (Q i - R i) ^ 2

The triangle inequality for a family of deviations, at the usual cost of a factor two.

theorem MIPRE.sum_snorm_sq_triangle3 {N : Type u_1} [Fintype N] [DecidableEq N] {κ : Type u_2} [Fintype κ] (v : N → ℂ) (P Q R T : κ → Matrix N N ℂ) : ∑ o : κ, snorm v (P o - T o) ^ 2 ≤ 3 * ∑ o : κ, snorm v (P o - Q o) ^ 2 + 3 * ∑ o : κ, snorm v (Q o - R o) ^ 2 + 3 * ∑ o : κ, snorm v (R o - T o) ^ 2

The three-term triangle inequality for a family of deviations.

theorem MIPRE.sum_weighted_snorm_sq_triangle3 {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} {κ : Type u_3} [Fintype κ] (v : N → ℂ) {w : ι → ℝ} (hw : ∀ (i : ι), 0 ≤ w i) (S : Finset ι) (P Q R T : ι → κ → Matrix N N ℂ) : ∑ i ∈ S, w i * ∑ o : κ, snorm v (P i o - T i o) ^ 2 ≤ 3 * ∑ i ∈ S, w i * ∑ o : κ, snorm v (P i o - Q i o) ^ 2 + 3 * ∑ i ∈ S, w i * ∑ o : κ, snorm v (Q i o - R i o) ^ 2 + 3 * ∑ i ∈ S, w i * ∑ o : κ, snorm v (R i o - T i o) ^ 2

The weighted form, over a set of questions: the shape every item of lem:qld-win is stated in.

A projective measurement is a POVM

def MIPRE.IsPVM.toPOVM {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] [DecidableEq Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) : POVM Λ n

A projective measurement, as a POVM. The same bridge as ProjectiveMeasurement.toPOVM, for the bare-family form IsPVM that the rigidity arguments produce.

Equations

• h.toPOVM = { mats := fun (a : Λ) => ⟨P a, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.IsPVM.toPOVM_mats {n : Type u_1} {Λ : Type u_2} [Fintype n] [DecidableEq n] [Fintype Λ] [DecidableEq Λ] {P : Λ → Matrix n n ℂ} (h : IsPVM P) (a : Λ) : ↑(h.toPOVM.mats a) = P a

Replacing one side of a cross-party deviation

theorem MIPRE.sum_xSqNorm_le_of_two_step {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {κ : Type u_3} [Fintype κ] {ψ : dA × dB → ℂ} (Q Q' : κ → Matrix dA dA ℂ) (R : κ → Matrix dB dB ℂ) {a b : ℝ} (h1 : ∑ o : κ, stateSqNorm ψ (Q o - Q' o) ≤ a) (h2 : ∑ o : κ, xSqNorm ψ (Q' o) (R o) ≤ b) : ∑ o : κ, xSqNorm ψ (Q o) (R o) ≤ 2 * a + 2 * b

Replacing Alice's operator by a nearby one on her own factor, inside a cross-party deviation: one triangle inequality, at the usual cost of a factor two.

Marginals of a coarse-grained POVM

theorem MIPRE.POVM.sum_mats_map_prod {d : Type u_1} [Fintype d] [DecidableEq d] {ι : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (M : POVM ι d) (f : ι → B) (g : ι → C) (b : B) : ∑ c : C, ↑((map (fun (a : ι) => (f a, g a)) M).mats (b, c)) = ↑((map f M).mats b)

The marginal of a jointly coarse-grained POVM is the coarse-graining of one component. sum_c (M.map (f, g))_{b,c} = (M.map f)_b: the fibres of (f, g) over {b} x C partition the fibre of f over b.

theorem MIPRE.POVM.sum_mats_map_prod' {d : Type u_1} [Fintype d] [DecidableEq d] {ι : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (M : POVM ι d) (f : ι → B) (g : ι → C) (c : C) : ∑ b : B, ↑((map (fun (a : ι) => (f a, g a)) M).mats (b, c)) = ↑((map g M).mats c)

The other marginal.

The two hypotheses of the steps, for the operators they are applied to

theorem MIPRE.aOp_mono {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {X Y : Matrix dA dA ℂ} (h : X ≤ Y) : aOp X ≤ aOp Y

theorem MIPRE.bOp_mono {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {X Y : Matrix dB dB ℂ} (h : X ≤ Y) : bOp X ≤ bOp Y

theorem MIPRE.bOp_sum {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} (s : Finset ι) (f : ι → Matrix dB dB ℂ) : bOp (∑ i ∈ s, f i) = ∑ i ∈ s, bOp (f i)

theorem MIPRE.sum_aOp_conjTranspose_mul_self_le_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} [Fintype ι] (A : POVM ι dA) : ∑ i : ι, (aOp ↑(A.mats i)).conjTranspose * aOp ↑(A.mats i) ≤ 1

A POVM on Alice's factor satisfies the hypothesis of sum_snorm_sq_mul_le. No projectivity: A^dag A = A^2 <= A and the elements sum to one.

theorem MIPRE.sum_bOp_conjTranspose_mul_self_le_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} [Fintype ι] (B : POVM ι dB) : ∑ i : ι, (bOp ↑(B.mats i)).conjTranspose * bOp ↑(B.mats i) ≤ 1

Bob's version.

theorem MIPRE.sum_bOp_conjTranspose_mul_self_of_isPVM {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {Q : ι → Matrix dB dB ℂ} (h : IsPVM Q) : ∑ i : ι, (bOp (Q i)).conjTranspose * bOp (Q i) = 1

A projective family on Bob's factor satisfies the hypothesis of sum_snorm_sq_mul_le with equality.

The marginals of a projective measurement with a product outcome set

theorem MIPRE.IsPVM.marg_mul_marg {N : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype N] [DecidableEq N] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {P : B × C → Matrix N N ℂ} (h : IsPVM P) (b : B) (c : C) : (∑ b' : B, P (b', c)) * ∑ c' : C, P (b, c') = P (b, c)

The two marginals of a projective measurement multiply to the joint element. This is the whole use of projectivity in the commutation analysis: the off-diagonal terms of the product vanish by IsPVM.orthogonal, and the surviving one is idempotent.

theorem MIPRE.IsPVM.sum_marg_left {N : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype N] [DecidableEq N] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {P : B × C → Matrix N N ℂ} (h : IsPVM P) : ∑ b : B, ∑ c : C, P (b, c) = 1

The marginal over C, as the coarse-graining of P that forgets the second outcome.

theorem MIPRE.IsPVM.sum_marg_right {N : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype N] [DecidableEq N] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {P : B × C → Matrix N N ℂ} (h : IsPVM P) : ∑ c : C, ∑ b : B, P (b, c) = 1

theorem MIPRE.IsPVM.marg_left {N : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype N] [DecidableEq N] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {P : B × C → Matrix N N ℂ} (h : IsPVM P) : IsPVM fun (b : B) => ∑ c : C, P (b, c)

The marginal of a projective measurement with a product outcome set is projective.

theorem MIPRE.IsPVM.marg_right {N : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype N] [DecidableEq N] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {P : B × C → Matrix N N ℂ} (h : IsPVM P) : IsPVM fun (c : C) => ∑ b : B, P (b, c)

theorem MIPRE.IsPVM.marg_mul_marg' {N : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype N] [DecidableEq N] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {P : B × C → Matrix N N ℂ} (h : IsPVM P) (b : B) (c : C) : (∑ c' : C, P (b, c')) * ∑ b' : B, P (b', c) = P (b, c)

The other order.

The analysis

Stated for abstract families in one algebra --- the two parties enter only through the hypotheses hcomm, hcomm' (the factors commute) and hmul, hmul' (Bob's two marginals multiply to the joint element). That keeps the algebra in a single type, and commutation_analysis below is the instance where the families are aOp and bOp of a POVM and a projective measurement, through BipartiteModel.commutation_analysis in the tensor-product model.

theorem MIPRE.sum_prod_snorm_sq_mul_le_fst {N : Type u_1} [Fintype N] [DecidableEq N] {B : Type u_2} {C : Type u_3} [Fintype B] [Fintype C] (v : N → ℂ) (F : B → Matrix N N ℂ) (hF : ∑ b : B, (F b).conjTranspose * F b ≤ 1) (M : C → Matrix N N ℂ) : ∑ p : B × C, snorm v (F p.1 * M p.2) ^ 2 ≤ ∑ c : C, snorm v (M c) ^ 2

Putting a family in front, with the front index in the first component of the pair.

theorem MIPRE.sum_prod_snorm_sq_mul_le_snd {N : Type u_1} [Fintype N] [DecidableEq N] {B : Type u_2} {C : Type u_3} [Fintype B] [Fintype C] (v : N → ℂ) (F : C → Matrix N N ℂ) (hF : ∑ c : C, (F c).conjTranspose * F c ≤ 1) (M : B → Matrix N N ℂ) : ∑ p : B × C, snorm v (F p.2 * M p.1) ^ 2 ≤ ∑ b : B, snorm v (M b) ^ 2

Putting a family in front, with the front index in the second component.

theorem MIPRE.commutation_analysis_abstract {N : Type u_1} [Fintype N] [DecidableEq N] {B : Type u_2} {C : Type u_3} [Fintype B] [Fintype C] {δ : ℝ} (v : N → ℂ) (alpha : B → Matrix N N ℂ) (gamma : C → Matrix N N ℂ) (betaB : B → Matrix N N ℂ) (betaC : C → Matrix N N ℂ) (betaBC : B × C → Matrix N N ℂ) (halpha : ∑ b : B, (alpha b).conjTranspose * alpha b ≤ 1) (hgamma : ∑ c : C, (gamma c).conjTranspose * gamma c ≤ 1) (hbetaB : ∑ b : B, (betaB b).conjTranspose * betaB b ≤ 1) (hbetaC : ∑ c : C, (betaC c).conjTranspose * betaC c ≤ 1) (hcomm : ∀ (b : B) (c : C), alpha b * betaC c = betaC c * alpha b) (hcomm' : ∀ (b : B) (c : C), gamma c * betaB b = betaB b * gamma c) (hmul : ∀ (b : B) (c : C), betaC c * betaB b = betaBC (b, c)) (hmul' : ∀ (b : B) (c : C), betaB b * betaC c = betaBC (b, c)) (hA : ∑ b : B, snorm v (alpha b - betaB b) ^ 2 ≤ δ) (hC : ∑ c : C, snorm v (gamma c - betaC c) ^ 2 ≤ δ) : ∑ p : B × C, snorm v (alpha p.1 * gamma p.2 - gamma p.2 * alpha p.1) ^ 2 ≤ 16 * δ

The commutation analysis, in one algebra: StateModel.commutation_analysis_abstract in the matrix model.

The instance: a POVM pair on Alice against a projective measurement on Bob

theorem MIPRE.commutation_analysis {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {B : Type u_3} {C : Type u_4} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {ψ : dA × dB → ℂ} {A : POVM B dA} {Cm : POVM C dA} {P : B × C → Matrix dB dB ℂ} (hP : IsPVM P) {δ : ℝ} (hA : ∑ b : B, snorm ψ (aOp ↑(A.mats b) - bOp (∑ c : C, P (b, c))) ^ 2 ≤ δ) (hC : ∑ c : C, snorm ψ (aOp ↑(Cm.mats c) - bOp (∑ b : B, P (b, c))) ^ 2 ≤ δ) : ∑ p : B × C, snorm ψ (aOp ↑(A.mats p.1) * aOp ↑(Cm.mats p.2) - aOp ↑(Cm.mats p.2) * aOp ↑(A.mats p.1)) ^ 2 ≤ 16 * δ

The commutation analysis (lem:commutation-analysis). Two POVMs on Alice's factor, each cross-party close to the corresponding marginal of one projective measurement on Bob's, commute on the state at 16 delta.

theorem MIPRE.commutation_analysis_aOp {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {B : Type u_3} {C : Type u_4} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] {ψ : dA × dB → ℂ} {A : POVM B dA} {Cm : POVM C dA} {P : B × C → Matrix dB dB ℂ} (hP : IsPVM P) {δ : ℝ} (hA : ∑ b : B, snorm ψ (aOp ↑(A.mats b) - bOp (∑ c : C, P (b, c))) ^ 2 ≤ δ) (hC : ∑ c : C, snorm ψ (aOp ↑(Cm.mats c) - bOp (∑ b : B, P (b, c))) ^ 2 ≤ δ) : ∑ p : B × C, snorm ψ (aOp (↑(A.mats p.1) * ↑(Cm.mats p.2) - ↑(Cm.mats p.2) * ↑(A.mats p.1))) ^ 2 ≤ 16 * δ

The commutator form, with the difference inside a single aOp.

From the POVM elements to the observables

The last step of the paper's commuting case: expanding a two-outcome observable as Id - 2 M_1, the commutator of two such observables is exactly four times the commutator of the two M_1's, because the identity commutes with everything. So the transfer costs a factor 16 in the squared norm and no approximation at all.

theorem MIPRE.obs2_commutator_eq {d : Type u_5} [Fintype d] [DecidableEq d] (A Cm : POVM (ZMod 2) d) : obs2 A * obs2 Cm - obs2 Cm * obs2 A = 4 • (↑(A.mats 1) * ↑(Cm.mats 1) - ↑(Cm.mats 1) * ↑(A.mats 1))