Bridge, part 8: the soundness theorem in our vocabulary

The main theorem MIPStarRE.LDT.Test.mainFormal, applied to the induced strategy toProjStrat S, produces two MIPStarRE projective measurements with outcomes in the polynomials of individual degree at most d; ofProjMeas reads them as our projective measurements with outcomes in LowIndDegPoly, and the three consistency conclusions are transferred with inconsistency_eq_bipartiteConsError.

noncomputable def MIPRE.LIDT.Bridge.ofProjMeas {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (G : MIPStarRE.LDT.ProjMeas (MIPStarRE.LDT.Polynomial (lidtParams F m d)) n) : ProjectiveMeasurement Unit LowIndDegPoly (Matrix n n ℂ)

A MIPStarRE projective measurement with polynomial outcomes, as one of our projective measurements (over the one-element question alphabet) with outcomes in LowIndDegPoly.

Equations

• MIPRE.LIDT.Bridge.ofProjMeas G = { M := fun (x : Unit) (c : MIPRE.LIDT.LowIndDegPoly) => G.outcome (MIPRE.LIDT.Bridge.lowIndDegEquiv c), selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.LIDT.Bridge.ofProjMeas_M {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (G : MIPStarRE.LDT.ProjMeas (MIPStarRE.LDT.Polynomial (lidtParams F m d)) n) (c : LowIndDegPoly) : (ofProjMeas G).M () c = G.outcome (lowIndDegEquiv c)

theorem MIPRE.LIDT.Bridge.mainFormalError_eq {F : Type u_1} [Field F] [Fintype F] {m d : ℕ} [NeZero m] (k : ℕ) (ε : ℝ) : MIPStarRE.LDT.Test.mainFormalError (lidtParams F m d) k ε = lidtError m d (Fintype.card F) k ε

The error bounds of the two developments agree.

theorem MIPRE.LIDT.Bridge.pointPOVMA_val {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) (u : Point F m) (a : F) : ↑((pointPOVMA S u).mats a) = ((toProjStrat S).pointMeasurementA (encP u)).outcome (enc a)

The point POVMs of player A, as outcomes of the induced strategy's point measurements.

theorem MIPRE.LIDT.Bridge.pointPOVMB_val {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) (u : Point F m) (a : F) : ↑((pointPOVMB S u).mats a) = ((toProjStrat S).pointMeasurementB (encP u)).outcome (enc a)

The point POVMs of player B, as outcomes of the induced strategy's point measurements.

theorem MIPRE.LIDT.Bridge.evalPOVM_val {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {n : Type u_2} [Fintype n] [DecidableEq n] (G : MIPStarRE.LDT.ProjMeas (MIPStarRE.LDT.Polynomial (lidtParams F m d)) n) (u : Point F m) (a : F) : ↑((evalPOVM (ofProjMeas G) u).mats a) = (MIPStarRE.LDT.polynomialEvaluationFamily (lidtParams F m d) G.toSubMeas (encP u)).outcome (enc a)

Evaluation of a converted global measurement, as MIPStarRE's evaluation family.

theorem MIPRE.LIDT.Bridge.soundness {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) (ε : ℝ) (hS : 1 - ε ≤ S.value) (k : ℕ) (hk : 400 * m * d ≤ k) (hk0 : 0 < k) : ∃ (GA : ProjectiveMeasurement Unit LowIndDegPoly (Matrix (Fin S.dA) (Fin S.dA) ℂ)) (GB : ProjectiveMeasurement Unit LowIndDegPoly (Matrix (Fin S.dB) (Fin S.dB) ℂ)), inconsistency (uniform (Point F m)) S.ψ (pointPOVMA S) (evalPOVM GB) ≤ lidtError m d (Fintype.card F) k ε ∧ inconsistency (uniform (Point F m)) S.ψ (evalPOVM GA) (pointPOVMB S) ≤ lidtError m d (Fintype.card F) k ε ∧ (inconsistency (uniform Unit) S.ψ (fun (x : Unit) => GA.toPOVM ()) fun (x : Unit) => GB.toPOVM ()) ≤ lidtError m d (Fintype.card F) k ε

The soundness theorem, assembled from the MIPStarRE main theorem.