The disagreement of two parties' measurements

The probability dis ψ M N = 1 - ∑_a ⟨ψ| M_a ⊗ N_a |ψ⟩ that Alice's POVM M and Bob's N, measured on ψ, return different outcomes, and four facts about it that the soundness of answer reduction uses throughout:

• it only decreases under a common coarse-graining (dis_map_le);
• disagreements chain across the two parties, linearly (sum_dis_triangle, from agreeSum_triangle): Alice's A against Bob's D through Bob's B and Alice's C;
• the probability of an event under Alice's measurement is at most its probability under Bob's, plus their disagreement (sum_ite_bornProb_one_le): no square root is lost, and the two measurements need not be projective;
• a subtest whose acceptance forces the agreement of two readings of the answers bounds their disagreement by its conditional failure, and a subtest whose acceptance excludes an event bounds that event's probability by it (sum_ite_bornProb_le_condFail).

All of it is proved once, for a bipartite model (BipartiteModel.dis and the lemmas after it), and the matrix statements are the instances in the tensor-product model (dis_eq_tensor).

In a bipartite model

The disagreement and its facts, for a bipartite model with the players' POVMs in their ordered algebras; the matrix statements below are the instances in the tensor-product model (dis_eq_tensor).

def MIPRE.BipartiteModel.dis {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) : ℝ

The disagreement of the first player's POVM P and the second player's Q: the probability that their outcomes differ.

Equations

• M.dis P Q = 1 - ∑ a : Λ, M.bornProb (P.op a) (Q.op a)

theorem MIPRE.BipartiteModel.bornProb_one_right {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] {Λ : Type u_4} [Fintype Λ] (e : 𝒜) (Q : POVMIn Λ ℬ) : M.bornProb e 1 = ∑ b : Λ, M.bornProb e (Q.op b)

theorem MIPRE.BipartiteModel.bornProb_one_left {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ 𝒜) (f : ℬ) : M.bornProb 1 f = ∑ a : Λ, M.bornProb (P.op a) f

theorem MIPRE.BipartiteModel.sum_bornProb_diag_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (hψ : ‖M.ψ‖ = 1) (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) : ∑ a : Λ, M.bornProb (P.op a) (Q.op a) ≤ 1

theorem MIPRE.BipartiteModel.dis_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (hψ : ‖M.ψ‖ = 1) (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) : 0 ≤ M.dis P Q

theorem MIPRE.BipartiteModel.dis_map_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] {C : Type u_5} [Fintype C] [DecidableEq C] (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) (f : Λ → C) : M.dis (POVMIn.map f P) (POVMIn.map f Q) ≤ M.dis P Q

Data processing: a common coarse-graining can only decrease the disagreement.

theorem MIPRE.BipartiteModel.dis_eq_sum_ne {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {Λ : Type u_4} [Fintype Λ] (hψ : ‖M.ψ‖ = 1) [DecidableEq Λ] (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) : M.dis P Q = ∑ a : Λ, ∑ b : Λ, if a = b then 0 else M.bornProb (P.op a) (Q.op b)

The disagreement is the sum of the off-diagonal Born probabilities.

theorem MIPRE.BipartiteModel.sum_ite_bornProb_one_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (hψ : ‖M.ψ‖ = 1) [DecidableEq Λ] (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) (E : Λ → Prop) [DecidablePred E] : (∑ a : Λ, if E a then M.bornProb (P.op a) 1 else 0) ≤ (∑ b : Λ, if E b then M.bornProb 1 (Q.op b) else 0) + M.dis P Q

An event transfers across the parties: its probability under the first player's measurement is at most its probability under the second player's plus their disagreement.

theorem MIPRE.BipartiteModel.sum_ite_bornProb_one_le' {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (hψ : ‖M.ψ‖ = 1) [DecidableEq Λ] (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) (E : Λ → Prop) [DecidablePred E] : (∑ b : Λ, if E b then M.bornProb 1 (Q.op b) else 0) ≤ (∑ a : Λ, if E a then M.bornProb (P.op a) 1 else 0) + M.dis P Q

The mirror image: an event transfers from the second player's measurement to the first's.

theorem MIPRE.BipartiteModel.dis_map_eq_sum {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hψ : ‖M.ψ‖ = 1) {A : Type u_5} {B : Type u_6} {C : Type u_7} [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] (P : POVMIn A 𝒜) (Q : POVMIn B ℬ) (f : A → C) (g : B → C) : M.dis (POVMIn.map f P) (POVMIn.map g Q) = ∑ a : A, ∑ b : B, (if f a = g b then 0 else 1) * M.bornProb (P.op a) (Q.op b)

The disagreement of two readings is the weight of the outcome pairs they read differently.

theorem MIPRE.BipartiteModel.dis_le_sum_dis_map_add {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (hψ : ‖M.ψ‖ = 1) [DecidableEq Λ] (P : POVMIn Λ 𝒜) (Q : POVMIn Λ ℬ) {Y : Type u_5} {R : Type u_6} [Fintype Y] [Fintype R] [DecidableEq R] {ν : Y → ℝ} (hν0 : ∀ (y : Y), 0 ≤ ν y) (hν1 : ∑ y : Y, ν y = 1) (ev : Y → Λ → R) {ε : ℝ} (hε : 0 ≤ ε) (hsep : ∀ (g g' : Λ), g ≠ g' → (∑ y : Y, ν y * if ev y g = ev y g' then 1 else 0) ≤ ε) : M.dis P Q ≤ ∑ y : Y, ν y * M.dis (POVMIn.map (ev y) P) (POVMIn.map (ev y) Q) + ε

From evaluations to outcomes: when distinct outcomes are separated by an evaluation map at a point drawn from ν, colliding with probability at most ε, the disagreement of the outcomes is at most the average disagreement of the evaluations, plus ε. Neither measurement need be projective.

Families on a uniform index

theorem MIPRE.BipartiteModel.one_sub_agreeSum_uniform {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {Λ : Type u_4} [Fintype Λ] {X : Type u_5} [Fintype X] [Nonempty X] (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : 1 - M.agreeSum (uniform X) P Q = (∑ x : X, M.dis (P x) (Q x)) / ↑(Fintype.card X)

theorem MIPRE.BipartiteModel.sum_dis_triangle {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] {X : Type u_5} [Fintype X] [Nonempty X] (hψ : ‖M.ψ‖ = 1) (A C : X → POVMIn Λ 𝒜) (B D : X → POVMIn Λ ℬ) : ∑ x : X, M.dis (A x) (D x) ≤ 11 * (∑ x : X, M.dis (A x) (B x) + ∑ x : X, M.dis (C x) (B x) + ∑ x : X, M.dis (C x) (D x))

The disagreement triangle across the two parties, on a uniform index: the first player's A against the second player's D, through the second player's B and the first player's C.

Subtests

theorem MIPRE.BipartiteModel.dis_map_le_condFail {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} {C : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} {x : X} {y : Y} (f : A → C) (g : B → C) (hD : ∀ (a : A) (b : B), G.D x y a b = true → f a = g b) : M.dis (POVMIn.map f (MA x)) (POVMIn.map g (MB y)) ≤ M.condFail G MA MB x y

An agreement subtest bounds the disagreement of the two readings.

theorem MIPRE.BipartiteModel.sum_ite_bornProb_le_condFail {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (hψ : ‖M.ψ‖ = 1) {x : X} {y : Y} (E : B → Prop) [DecidablePred E] (hD : ∀ (a : A) (b : B), G.D x y a b = true → ¬E b) : (∑ b : B, if E b then M.bornProb 1 ((MB y).op b) else 0) ≤ M.condFail G MA MB x y

A subtest excluding an event of the second player's answer bounds its probability.

theorem MIPRE.BipartiteModel.sum_ite_bornProb_le_condFail' {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (hψ : ‖M.ψ‖ = 1) {x : X} {y : Y} (E : A → Prop) [DecidablePred E] (hD : ∀ (a : A) (b : B), G.D x y a b = true → ¬E a) : (∑ a : A, if E a then M.bornProb ((MA x).op a) 1 else 0) ≤ M.condFail G MA MB x y

The mirror image, for an event of the first player's answer.

theorem MIPRE.BipartiteModel.condFail_le_of {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} {C : Type u_9} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (hψ : ‖M.ψ‖ = 1) {x : X} {y : Y} (EA : A → Prop) (EB : B → Prop) [DecidablePred EA] [DecidablePred EB] (f : A → C) (g : B → C) (hD : ∀ (a : A) (b : B), ¬EA a → ¬EB b → f a = g b → G.D x y a b = true) : M.condFail G MA MB x y ≤ ((∑ a : A, if EA a then M.bornProb ((MA x).op a) 1 else 0) + ∑ b : B, if EB b then M.bornProb 1 ((MB y).op b) else 0) + M.dis (POVMIn.map f (MA x)) (POVMIn.map g (MB y))

A subtest accepting when two events are avoided and two readings agree fails at most the events' probabilities plus the readings' disagreement.

def MIPRE.dis {Λ : Type u_1} [Fintype Λ] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : POVM Λ dA) (N : POVM Λ dB) : ℝ

The disagreement of Alice's POVM M and Bob's POVM N on the state ψ: the probability that their outcomes differ.

Equations

• MIPRE.dis ψ M N = 1 - ∑ a : Λ, MIPRE.bornProb ψ ↑(M.mats a) ↑(N.mats a)

theorem MIPRE.dis_eq_tensor {Λ : Type u_1} [Fintype Λ] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : POVM Λ dA) (N : POVM Λ dB) : dis ψ M N = (BipartiteModel.tensor ψ).dis M.toIn N.toIn

The matrix disagreement is that of the tensor-product model.

Families on a uniform index

Subtests