Bridge, part 7: consistency #
Our inconsistency μ ψ M N = 𝔼_{x∼μ} ∑_{a≠b} ⟨ψ| M^x_a ⊗ N^x_b |ψ⟩ for families of
POVMs, versus MIPStarRE's bipartiteConsError ψ 𝒟 A B, an average of
max 0 (⟨A_tot ⊗ B_tot⟩ − ∑ₐ ⟨A_a ⊗ B_a⟩) over a weighted distribution. For complete
measurements, uniform distributions, and the pure state of a strategy, the two agree once
questions and outcomes are matched along equivalences (inconsistency_eq_bipartiteConsError).
theorem
MIPRE.LIDT.Bridge.inconsistency_eq_bipartiteConsError
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
{X : Type u_2}
{X' : Type u_3}
{α : Type u_4}
{α' : Type u_5}
[Fintype X]
[Fintype X']
[DecidableEq X']
[Nonempty X']
[Fintype α]
[DecidableEq α]
[Fintype α']
(qe : X ≃ X')
(e : α ≃ α')
(M : X → POVM α (Fin S.dA))
(N : X → POVM α (Fin S.dB))
(A : MIPStarRE.LDT.IdxSubMeas X' α' (Fin S.dA))
(B : MIPStarRE.LDT.IdxSubMeas X' α' (Fin S.dB))
(hA : ∀ (x' : X'), (A x').total = 1)
(hB : ∀ (x' : X'), (B x').total = 1)
(hM : ∀ (x : X) (a : α), ↑((M x).mats a) = (A (qe x)).outcome (e a))
(hN : ∀ (x : X) (a : α), ↑((N x).mats a) = (B (qe x)).outcome (e a))
:
inconsistency (uniform X) S.ψ M N = MIPStarRE.LDT.bipartiteConsError (toProjStrat S).state (MIPStarRE.LDT.uniformDistribution X') A B
Our inconsistency of two POVM families agrees with MIPStarRE's consistency error of
two complete submeasurement families, when questions and outcomes are matched along
equivalences qe, e and the state is the pure state of a strategy.