Removing the dummy coordinates (lem:qld-global-dummy)

The global polynomial measurements of lem:qld-global-pvm have outcomes in LowIndDegPoly F (4m) d, polynomials in the 4m coordinates of the padded point, while the padded point measurements read only the 2m + 2 coordinates xBlk, zBlk, alph, bet (padPt_mats). The remaining 2m - 2 coordinates are the paper's dummy coordinates w. This file proves that an outcome which reads a dummy coordinate carries little state weight: if the evaluated global measurement is δ-consistent, on average over a uniform point, with a point measurement that does not read the dummy coordinates, then the total weight of such outcomes is at most 2δ / (1 - 8md/q), hence 4δ once 16 m d ≤ q.

The argument

Resample the dummy coordinates: for two independent uniform points u, u', let mix u u' be u with its dummy coordinates replaced by those of u'. The point measurement is the same at u and at mix u u', and (u, u') ↦ (mix u u', mix u' u) is an involution of the pairs, so the consistency estimate holds at both points simultaneously. Adding the two, the operator P_u(g(u)) + P_u(g(mix u u')) is at most 2 · 1 when the two values agree and at most 1 when they differ (two distinct elements of a POVM sum to at most the identity; no projectivity is used), which gives ∑_g ⟨G_g⟩ · Pr[g(u) = g(mix u u')] ≥ 1 - 2δ (sum_mass_mixAgree_ge). For an outcome that reads a dummy coordinate, g(u) - g(mix u u') is a nonzero polynomial in the 8m coordinates of the pair, of individual degree at most d, so Schwartz--Zippel bounds the probability by 8md/q (card_mixAgree_le); for one that does not, the probability is 1 (eval_mix_of_wIndep). The two bounds give sum_bad_mass_le.

The bridge to MvPolynomial

LowIndDegPoly.toMv, degreeOf_rename_le and prob_agreeOn_le_individualDegree (Schwartz--Zippel for any finite variable type, which is what the pair Fin (4m) ⊕ Fin (4m) needs) were written here and now live in MIPRE/Background/LIDT/Coefficients.lean, where the simultaneous low-degree test can use them too.

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 low individual degree test is applied, padModel, or any other --- the global measurement is a POVM G in the first player's algebra (POVMIn), evaluated at a point by evalPOVMIn, the point measurement is a family of POVMs in the second player's algebra, and the weight of an outcome is the Born probability K.bornProb (G.op g) 1. That two distinct elements of a POVM sum to at most one holds in any star-ordered ring (POVMIn.add_le_one), and the elements of G are nonnegative as those of a POVM, so neither measurement needs to be projective. The second player's version is the first player's in the exchanged model K.swap (BipartiteModel.inconsistency_swap, BipartiteModel.bornProb_swap). The polynomial half is unchanged.

Born-rule and POVM facts

theorem MIPRE.bornProb_add_right {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (X : 𝒜) (Y Z : ℬ) : M.bornProb X (Y + Z) = M.bornProb X Y + M.bornProb X Z

The Born probability is additive in the second player's operator.

theorem MIPRE.POVMIn.add_le_one {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {A : Type u_2} [Fintype A] [DecidableEq A] (M : POVMIn A R) {b b' : A} (h : b ≠ b') : M.op b + M.op b' ≤ 1

Two distinct elements of a POVM sum to at most one, in any star-ordered ring.

theorem MIPRE.sum_ite_eq_zero_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup β] (a : α) (x : α → β) : (∑ b : α, if a = b then 0 else x b) = ∑ b : α, x b - x a

The inconsistency of an evaluated global measurement, unfolded

def MIPRE.QLD.evalPOVMIn {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn LIDT.LowIndDegPoly R) (u : LIDT.Point F n) : POVMIn F R

A global measurement evaluated at a point: the POVM with outcomes in F whose element at a is the sum of the elements at the polynomials g with g(u) = a. The model form of LIDT.evalPOVM, in any star-ordered ring.

Equations

• MIPRE.QLD.evalPOVMIn G u = MIPRE.POVMIn.map (fun (g : MIPRE.LIDT.LowIndDegPoly) => g.eval u) G

theorem MIPRE.QLD.evalPOVMIn_op {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn LIDT.LowIndDegPoly R) (u : LIDT.Point F n) (a : F) : (evalPOVMIn G u).op a = ∑ g : LIDT.LowIndDegPoly with g.eval u = a, G.op g

theorem MIPRE.QLD.inconsistency_evalPOVM_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] [StarOrderedRing 𝒜] (μ : LIDT.Point F n → ℝ) (hμ : ∑ u : LIDT.Point F n, μ u = 1) {K : BipartiteModel 𝒞 𝒜 ℬ} (hK : ‖K.ψ‖ = 1) (G : POVMIn LIDT.LowIndDegPoly 𝒜) (P : LIDT.Point F n → POVMIn F ℬ) : K.inconsistency μ (evalPOVMIn G) P = 1 - ∑ u : LIDT.Point F n, μ u * ∑ g : LIDT.LowIndDegPoly, K.bornProb (G.op g) ((P u).op (g.eval u))

The inconsistency of an evaluated global measurement with a point measurement is one minus the average weight the global outcome's value at the point receives from the point measurement: 1 - ∑_u μ_u ∑_g ⟨G_g ⊗ P_u(g(u))⟩.

theorem MIPRE.QLD.sum_bornProb_M_one {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] {K : BipartiteModel 𝒞 𝒜 ℬ} (hK : ‖K.ψ‖ = 1) {A : Type u_5} [Fintype A] (G : POVMIn A 𝒜) : ∑ g : A, K.bornProb (G.op g) 1 = 1

The total weight of a POVM's outcomes is one.

The dummy coordinates

def MIPRE.QLD.IsDummy {m : ℕ} (i : Fin (4 * m)) : Prop

A coordinate of the padded point that no padded point measurement reads: everything past xBlk, zBlk, alph, bet.

Equations

• MIPRE.QLD.IsDummy i = (2 * m + 2 ≤ ↑i)

@[instance_reducible]

instance MIPRE.QLD.instDecidablePredFinHMulNatOfNatIsDummy {m : ℕ} : DecidablePred IsDummy

Equations

• MIPRE.QLD.instDecidablePredFinHMulNatOfNatIsDummy i = { decide := (2 * m + 2).ble ↑i, reflects_decide := ⋯ }

theorem MIPRE.QLD.not_isDummy_xIdx {m : ℕ} [NeZero m] (i : Fin m) : ¬IsDummy (xIdx m i)

theorem MIPRE.QLD.not_isDummy_zIdx {m : ℕ} [NeZero m] (i : Fin m) : ¬IsDummy (zIdx m i)

theorem MIPRE.QLD.not_isDummy_aIdx {m : ℕ} [NeZero m] : ¬IsDummy (aIdx m)

theorem MIPRE.QLD.not_isDummy_bIdx {m : ℕ} [NeZero m] : ¬IsDummy (bIdx m)

theorem MIPRE.QLD.not_isDummy_of_eq_one {m : ℕ} (hm : m = 1) (i : Fin (4 * m)) : ¬IsDummy i

For m = 1 there are no dummy coordinates.

def MIPRE.QLD.mix {F : Type u_1} {m : ℕ} (u u' : LIDT.Point F (4 * m)) : LIDT.Point F (4 * m)

Resampling the dummy coordinates: u with its dummy coordinates replaced by those of u'.

Equations

• MIPRE.QLD.mix u u' i = if MIPRE.QLD.IsDummy i then u' i else u i

theorem MIPRE.QLD.mix_apply_of_not {F : Type u_1} {m : ℕ} (u u' : LIDT.Point F (4 * m)) {i : Fin (4 * m)} (h : ¬IsDummy i) : mix u u' i = u i

theorem MIPRE.QLD.mix_apply_of {F : Type u_1} {m : ℕ} (u u' : LIDT.Point F (4 * m)) {i : Fin (4 * m)} (h : IsDummy i) : mix u u' i = u' i

@[simp]

theorem MIPRE.QLD.xBlk_mix {F : Type u_1} {m : ℕ} [NeZero m] (u u' : LIDT.Point F (4 * m)) : xBlk (mix u u') = xBlk u

@[simp]

theorem MIPRE.QLD.zBlk_mix {F : Type u_1} {m : ℕ} [NeZero m] (u u' : LIDT.Point F (4 * m)) : zBlk (mix u u') = zBlk u

@[simp]

theorem MIPRE.QLD.alph_mix {F : Type u_1} {m : ℕ} [NeZero m] (u u' : LIDT.Point F (4 * m)) : alph (mix u u') = alph u

@[simp]

theorem MIPRE.QLD.bet_mix {F : Type u_1} {m : ℕ} [NeZero m] (u u' : LIDT.Point F (4 * m)) : bet (mix u u') = bet u

theorem MIPRE.QLD.mix_mix {F : Type u_1} {m : ℕ} (u u' : LIDT.Point F (4 * m)) : mix (mix u u') (mix u' u) = u

def MIPRE.QLD.mixSwap {F : Type u_1} {m : ℕ} : LIDT.Point F (4 * m) × LIDT.Point F (4 * m) ≃ LIDT.Point F (4 * m) × LIDT.Point F (4 * m)

The involution of pairs of points that exchanges their dummy coordinates.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.QLD.mixSwap_apply_fst {F : Type u_1} {m : ℕ} (p : LIDT.Point F (4 * m) × LIDT.Point F (4 * m)) : (mixSwap p).1 = mix p.1 p.2

theorem MIPRE.QLD.padPt_mix {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {S : Question F m → POVMIn (Answer F m d) R} (hS : ∀ (q : Question F m), IsPVMIn (S q).op) (u u' : LIDT.Point F (4 * m)) : padPt hS (mix u u') = padPt hS u

The padded point measurement does not read the dummy coordinates.

def MIPRE.QLD.WIndep {F : Type u_1} [Field F] {m d : ℕ} (g : LIDT.LowIndDegPoly) : Prop

w-independence: a coefficient vector with no monomial involving a dummy coordinate.

Equations

• MIPRE.QLD.WIndep g = ∀ (e : Fin (4 * m) → Fin (d + 1)), (∃ (i : Fin (4 * m)), MIPRE.QLD.IsDummy i ∧ e i ≠ 0) → g e = 0

@[instance_reducible]

instance MIPRE.QLD.instDecidablePredLowIndDegPolyWIndep {F : Type u_1} [Field F] [DecidableEq F] {m d : ℕ} : DecidablePred WIndep

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.QLD.wIndep_of_eq_one {F : Type u_1} [Field F] {m d : ℕ} (hm : m = 1) (g : LIDT.LowIndDegPoly) : WIndep g

theorem MIPRE.QLD.eval_mix_of_wIndep {F : Type u_1} [Field F] {m d : ℕ} {g : LIDT.LowIndDegPoly} (hg : WIndep g) (u u' : LIDT.Point F (4 * m)) : g.eval (mix u u') = g.eval u

A w-independent outcome takes the same value after resampling the dummy coordinates.

Schwartz--Zippel on the pair

def MIPRE.QLD.dumSub {m : ℕ} (i : Fin (4 * m)) : Fin (4 * m) ⊕ Fin (4 * m)

The substitution that reads the dummy coordinates from the second point of a pair.

Equations

• MIPRE.QLD.dumSub i = if MIPRE.QLD.IsDummy i then Sum.inr i else Sum.inl i

theorem MIPRE.QLD.dumSub_injective {m : ℕ} : Function.Injective dumSub

theorem MIPRE.QLD.comp_dumSub {F : Type u_1} {m : ℕ} (x : Fin (4 * m) ⊕ Fin (4 * m) → F) : x ∘ dumSub = mix (x ∘ Sum.inl) (x ∘ Sum.inr)

theorem MIPRE.QLD.rename_toMv_ne {F : Type u_1} [Field F] {m d : ℕ} {g : LIDT.LowIndDegPoly} (hg : ¬WIndep g) : (MvPolynomial.rename Sum.inl) g.toMv ≠ (MvPolynomial.rename dumSub) g.toMv

An outcome that reads a dummy coordinate is a different polynomial of the pair before and after the resampling.

def MIPRE.QLD.mixAgree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} (g : LIDT.LowIndDegPoly) : Finset (LIDT.Point F (4 * m) × LIDT.Point F (4 * m))

The pairs of points at which an outcome takes the same value before and after resampling the dummy coordinates.

Equations

• MIPRE.QLD.mixAgree g = {p : MIPRE.LIDT.Point F (4 * m) × MIPRE.LIDT.Point F (4 * m) | g.eval p.1 = g.eval (MIPRE.QLD.mix p.1 p.2)}

theorem MIPRE.QLD.mixAgree_eq_univ_of_wIndep {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {g : LIDT.LowIndDegPoly} (hg : WIndep g) : mixAgree g = Finset.univ

theorem MIPRE.QLD.card_mixAgree_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {g : LIDT.LowIndDegPoly} (hg : ¬WIndep g) : ↑(mixAgree g).card / ↑(Fintype.card F) ^ (4 * m + 4 * m) ≤ ↑(4 * m + 4 * m) * ↑d / ↑(Fintype.card F)

Schwartz--Zippel for the dummy coordinates: an outcome that reads a dummy coordinate takes the same value before and after the resampling with probability at most 8md/q.

The weight of the outcomes that read a dummy coordinate

theorem MIPRE.QLD.sum_mass_mixAgree_ge {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {K : BipartiteModel 𝒞 𝒜 ℬ} (hK : ‖K.ψ‖ = 1) (G : POVMIn LIDT.LowIndDegPoly 𝒜) (P : LIDT.Point F (4 * m) → POVMIn F ℬ) (hP : ∀ (u u' : LIDT.Point F (4 * m)), P (mix u u') = P u) {δ : ℝ} (hcons : K.inconsistency (uniform (LIDT.Point F (4 * m))) (evalPOVMIn G) P ≤ δ) : 1 - 2 * δ ≤ ∑ g : LIDT.LowIndDegPoly, K.bornProb (G.op g) 1 * (↑(mixAgree g).card / ↑(Fintype.card F) ^ (4 * m + 4 * m))

The resampling estimate. If the evaluated global measurement is δ-consistent, on average over a uniform point, with a point measurement that does not read the dummy coordinates, then ∑_g ⟨G_g⟩ · Pr[g(u) = g(mix u u')] ≥ 1 - 2δ: the consistency holds at u and at mix u u' simultaneously, and two distinct elements of a POVM sum to at most one.

theorem MIPRE.QLD.sum_bad_mass_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {K : BipartiteModel 𝒞 𝒜 ℬ} (hK : ‖K.ψ‖ = 1) (G : POVMIn LIDT.LowIndDegPoly 𝒜) (P : LIDT.Point F (4 * m) → POVMIn F ℬ) (hP : ∀ (u u' : LIDT.Point F (4 * m)), P (mix u u') = P u) {δ : ℝ} (hcons : K.inconsistency (uniform (LIDT.Point F (4 * m))) (evalPOVMIn G) P ≤ δ) : (1 - ↑(4 * m + 4 * m) * ↑d / ↑(Fintype.card F)) * ∑ g : LIDT.LowIndDegPoly with ¬WIndep g, K.bornProb (G.op g) 1 ≤ 2 * δ

lem:qld-global-dummy. If the evaluated global measurement is δ-consistent with a point measurement that does not read the dummy coordinates, the total weight of the outcomes that read one satisfies (1 - 8md/q) · weight ≤ 2δ.

theorem MIPRE.QLD.sum_bad_mass_le_of_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {K : BipartiteModel 𝒞 𝒜 ℬ} (hK : ‖K.ψ‖ = 1) (G : POVMIn LIDT.LowIndDegPoly 𝒜) (P : LIDT.Point F (4 * m) → POVMIn F ℬ) (hP : ∀ (u u' : LIDT.Point F (4 * m)), P (mix u u') = P u) {δ : ℝ} (hcons : K.inconsistency (uniform (LIDT.Point F (4 * m))) (evalPOVMIn G) P ≤ δ) (hq : 16 * m * d ≤ Fintype.card F) : ∑ g : LIDT.LowIndDegPoly with ¬WIndep g, K.bornProb (G.op g) 1 ≤ 4 * δ

lem:qld-global-dummy with the standing assumption 16 m d ≤ q: the weight of the outcomes that read a dummy coordinate is at most 4δ.