Bridge, part 5: consistency defects of complete measurements

Generic facts about MIPStarRE's bipartite consistency defect qBipartiteConsDefect ψ A B = max 0 (⟨A_tot ⊗ B_tot⟩ − ∑ₐ ⟨A_a ⊗ B_a⟩) when the measurements A, B are complete (total = 1) and the state is normalized:

• the defect is 1 − ∑ₐ ⟨A_a ⊗ B_a⟩, and equals the off-diagonal mass ∑_{a ≠ b} ⟨A_a ⊗ B_b⟩ (qBipartiteConsDefect_eq_offDiagonal);
• for coarse-grainings postprocess A f, postprocess B g, the matching mass is ∑_{a, b : f a = g b} ⟨A_a ⊗ B_b⟩ (qBipartiteMatchMass_postprocess), so the defect is bounded by 1 − acc whenever acc is a sum of some of the terms ⟨A_a ⊗ B_b⟩ with f a = g b (qBipartiteConsDefect_postprocess_le).

These are the two facts through which the game's acceptance probability (Bridge.Value) and our inconsistency (Bridge.Consistency) are compared with the MIPStarRE quantities.

theorem MIPRE.LIDT.Bridge.ev_opTensor_outcome_nonneg {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas β ιB) (a : α) (b : β) : 0 ≤ MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor (A.outcome a) (B.outcome b))

Expectation values of tensor products of measurement operators are nonnegative.

theorem MIPRE.LIDT.Bridge.sum_ev_opTensor_outcome {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas β ιB) (hA : A.total = 1) (hB : B.total = 1) : ∑ a : α, ∑ b : β, MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor (A.outcome a) (B.outcome b)) = 1

The total mass of two complete measurements on a normalized state is one.

theorem MIPRE.LIDT.Bridge.qBipartiteMatchMass_postprocess {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq γ] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas β ιB) (f : α → γ) (g : β → γ) : MIPStarRE.LDT.qBipartiteMatchMass ψ (MIPStarRE.LDT.postprocess A f) (MIPStarRE.LDT.postprocess B g) = ∑ a : α, ∑ b : β, if f a = g b then MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor (A.outcome a) (B.outcome b)) else 0

The matching mass of two coarse-grained measurements.

theorem MIPRE.LIDT.Bridge.qBipartiteMatchMass_le_one {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} [Fintype α] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas α ιB) (hA : A.total = 1) (hB : B.total = 1) : MIPStarRE.LDT.qBipartiteMatchMass ψ A B ≤ 1

The matching mass of two complete measurements is at most one.

theorem MIPRE.LIDT.Bridge.qBipartiteConsDefect_of_complete {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} [Fintype α] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas α ιB) (hA : A.total = 1) (hB : B.total = 1) : MIPStarRE.LDT.qBipartiteConsDefect ψ A B = 1 - MIPStarRE.LDT.qBipartiteMatchMass ψ A B

For complete measurements on a normalized state the defect is 1 − matching mass.

theorem MIPRE.LIDT.Bridge.qBipartiteConsDefect_eq_offDiagonal {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} [Fintype α] [DecidableEq α] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas α ιB) (hA : A.total = 1) (hB : B.total = 1) : MIPStarRE.LDT.qBipartiteConsDefect ψ A B = ∑ a : α, ∑ b : α, if a = b then 0 else MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor (A.outcome a) (B.outcome b))

For complete measurements on a normalized state the defect is the off-diagonal mass.

theorem MIPRE.LIDT.Bridge.qBipartiteConsDefect_postprocess_le {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq γ] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : MIPStarRE.LDT.SubMeas α ιA) (B : MIPStarRE.LDT.SubMeas β ιB) (hA : A.total = 1) (hB : B.total = 1) (f : α → γ) (g : β → γ) (D : α → β → Prop) [DecidableRel D] (hD : ∀ (a : α) (b : β), D a b → f a = g b) : MIPStarRE.LDT.qBipartiteConsDefect ψ (MIPStarRE.LDT.postprocess A f) (MIPStarRE.LDT.postprocess B g) ≤ 1 - ∑ a : α, ∑ b : β, if D a b then MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor (A.outcome a) (B.outcome b)) else 0

The defect of two coarse-grainings of complete measurements is at most 1 − acc for any acceptance mass acc made of terms that force equal coarse-grained outcomes.

Averages over uniform distributions

theorem MIPRE.LIDT.Bridge.bipartiteConsError_uniform {X : Type u_6} [Fintype X] [DecidableEq X] [Nonempty X] {ιA : Type u_7} {ιB : Type u_8} {α : Type u_9} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] (ψ : MIPStarRE.LDT.QuantumState (ιA × ιB)) (A : MIPStarRE.LDT.IdxSubMeas X α ιA) (B : MIPStarRE.LDT.IdxSubMeas X α ιB) : MIPStarRE.LDT.bipartiteConsError ψ (MIPStarRE.LDT.uniformDistribution X) A B = 1 / ↑(Fintype.card X) * ∑ x : X, MIPStarRE.LDT.qBipartiteConsDefect ψ (A x) (B x)

The consistency error under the uniform distribution is the average of the defects.