Completing the pair measurement and its evaluated marginals (lem:qld-global-complete, #
lem:qld-global-sandwich)
Stage 4 ends with the interface SimulPair (lem:qld-simultaneous): a projective measurement
with outcomes pairs (g_X, g_Z) of polynomials in m variables, whose evaluated marginals are
consistent with the opposite party's expanded point measurements. This file builds it from a
global measurement G with outcomes in LowIndDegPoly F (4m) d (the polynomials on the padded
point) and the estimates of stage 4b, abstractly: for a projective G of the first player and
two projective families X x, Z z of the second.
The completion #
A good outcome g = α g_X(x) + β g_Z(z) (IsGood) is relabelled by the pair (g_X, g_Z), read
off its two coefficient polynomials through LowIndDegPoly.blockPoly (a polynomial reading only
the x block, as a polynomial in m variables); every other outcome is sent to the fixed pair
(0, 0). This is a coarse-graining of G, so it is a complete projective measurement
(pairMeas, isPVM_pairMeas): the paper's completion by the orthogonal complement R, whose
weight is the weight of the non-good outcomes, bounded by lem:qld-global-separate.
The marginals #
From the products estimate ∑_g E_u ‖(G_g ⊗ (1 - B_u(g(u)))) Φ‖² ≤ Δ, the triangle inequality
and Cauchy--Schwarz give ∑_g E_u ‖(G_g ⊗ B_u(g(u))) Φ‖² ≥ 1 - 2√Δ
(one_sub_two_sqrt_le_sum_snorm_sq). For a good g and the order X_a Z_b, the fibre analysis
of lem:qld-global-separate bounds E_u ‖(G_g ⊗ B_u(g(u))) Φ‖² by 2/q · ⟨G_g⟩ plus the
diagonal weight E_z ⟨G_g ⊗ Z_{g_Z(z)}(z)⟩, and the non-good outcomes carry weight at most
δ_G; hence the Z marginal E_z ∑_g ⟨G_g ⊗ Z_{g_Z(z)}(z)⟩ ≥ 1 - 2√Δ - 2/q - δ_G
(marg_Z_ge), and the order Z_b X_a gives the X marginal. The consistency form
(inconsistency_evalMarg_Z_le, _X_le) is the same statement read through inconsistency.
The instance of SimulPair is in PaddedLIDT.lean.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The state is that of a
bipartite model K (the model in which the global measurements live), the global measurement is
a POVM G in the first player's algebra with IsPVMIn G.op, the families X x, Z z are
projective families of the second player's algebra, a Born probability is K.bornProb, and a
squared norm K.snorm (K.πA (G.op g) * K.πB B) ^ 2. The completed pair measurement is the
coarse-graining G.map (pairOf hd) in the same algebra, so it needs no transport to the shape of
SimulPair: the matrix associativity reindexing of the doubly extended registers
(isPVM_reindex, isPVM_reindex_povm, reindex_aOp_aOp, POVM.aOp_aOp_reindex) and the
matrix projective-measurement packaging (ProjectiveMeasurement.isPVM_M) are gone.
The pair of a good outcome #
The α coefficient of a good outcome reads only the x block.
The β coefficient of a good outcome reads only the z block.
The X polynomial of an outcome: its α coefficient read on the x block.
Equations
- MIPRE.QLD.gX hd g = MIPRE.LIDT.LowIndDegPoly.blockPoly (MIPRE.QLD.xIdx m) (MIPRE.QLD.gA hd g)
Instances For
The Z polynomial of an outcome: its β coefficient read on the z block.
Equations
- MIPRE.QLD.gZ hd g = MIPRE.LIDT.LowIndDegPoly.blockPoly (MIPRE.QLD.zIdx m) (MIPRE.QLD.gB hd g)
Instances For
The relabelling: a good outcome becomes its pair (g_X, g_Z), every other outcome the
fixed pair (0, 0).
Equations
- MIPRE.QLD.pairOf hd g = if MIPRE.QLD.IsGood g then (MIPRE.QLD.gX hd g, MIPRE.QLD.gZ hd g) else (0, 0)
Instances For
The completed pair measurement: the global measurement coarse-grained by the relabelling.
The non-good outcomes are absorbed into the pair (0, 0): the paper's complement R, added to a
fixed legal outcome.
Equations
- MIPRE.QLD.pairMeas hd G = MIPRE.POVMIn.map (MIPRE.QLD.pairOf hd) G
Instances For
The completed pair measurement is projective.
The evaluated marginal of the completed measurement is the global measurement coarse-grained by the evaluated component of the pair.
The inconsistency of a coarse-grained global measurement #
The inconsistency of a coarse-graining of a global measurement, against a family of
POVMs indexed by the same questions: one minus the average agreement, outcome by outcome of the
original measurement. inconsistency_evalPOVM_eq is the case of evaluation at the point.
The block marginals of the uniform padded point #
The z block of a uniform padded point is uniform.
The x block of a uniform padded point is uniform.
The evaluated marginals #
The products estimate bounds the weight through B from below: from
∑_g E_u ‖(G_g ⊗ (1 - B_u(g(u)))) Φ‖² ≤ Δ, the triangle inequality and Cauchy--Schwarz give
∑_g E_u ‖(G_g ⊗ B_u(g(u))) Φ‖² ≥ 1 - 2√Δ.
The Z marginal of the completed measurement tracks the second player's Z point
measurement: from the products estimate for the order X_a Z_b and the weight δ_G of the
non-good outcomes, E_z ∑_g ⟨G_g ⊗ Z_{g_Z(z)}(z)⟩ ≥ 1 - 2√Δ - 2/q - δ_G, where g_Z is the
second component of the relabelled outcome.
The X marginal, from the order Z_b X_a: the mirror image.
lem:qld-global-sandwich, the Z marginal in consistency form: the evaluated Z
marginal of the completed measurement against a family N whose elements are the Z z a.
lem:qld-global-sandwich, the X marginal in consistency form.