Bridge, part 6: the value of a strategy bounds the MIPStarRE failure probability #
MIPStarRE's hypothesis is a bound on lowIndividualDegreeFailureProbability, a
trace-based surrogate for the failure probability: an average, over the verifier's
samples, of consistency defects between coarse-grained measurements. Our hypothesis is
a bound on the value S.value of the strategy in the game. This file shows
(toProjStrat S).lowIndividualDegreeFailureProbability ≤ 1 - S.value.
The value is the sum over samples s of s.weight · acc s where acc s is the
acceptance probability given the questions of s (value_eq_sum). For each sample the
defect of the corresponding branch is at most the rejection probability 1 - acc s,
by qBipartiteConsDefect_postprocess_le, because acceptance forces the two
coarse-grained outcomes to agree (the coarse-graining of the line answer is its
evaluation at the sampled point, that of the point answer is its value). The branch
weights of the two developments agree, which gives the bound after reindexing the
sample spaces through the field coding.
The value as a sum over samples #
def
MIPRE.LIDT.Bridge.born
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(x y : Question F m)
(a b : Answer F m d)
:
The Born-rule probability of the answers (a, b) to the questions (x, y).
Equations
Instances For
theorem
MIPRE.LIDT.Bridge.born_eq_ev
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(x y : Question F m)
(a b : Answer F m d)
:
born S x y a b = MIPStarRE.LDT.ev (toProjStrat S).state (MIPStarRE.LDT.opTensor (S.PA.M x a) (S.PB.M y b))
noncomputable def
MIPRE.LIDT.Bridge.acc
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(x y : Question F m)
:
The acceptance probability given the questions (x, y).
Equations
- MIPRE.LIDT.Bridge.acc S x y = ∑ a : MIPRE.LIDT.Answer F m d, ∑ b : MIPRE.LIDT.Answer F m d, if MIPRE.LIDT.accepts F m d x y a b = true then MIPRE.LIDT.Bridge.born S x y a b else 0
Instances For
Pointwise bounds #
theorem
MIPRE.LIDT.Bridge.defect_le_rej
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(x y : Question F m)
(f g : Answer F m d → MIPStarRE.LDT.Fq (lidtParams F m d))
(hD : ∀ (a b : Answer F m d), accepts F m d x y a b = true → f a = g b)
:
MIPStarRE.LDT.qBipartiteConsDefect (toProjStrat S).state (MIPStarRE.LDT.postprocess (toProjMeas S.PA x).toSubMeas f)
(MIPStarRE.LDT.postprocess (toProjMeas S.PB y).toSubMeas g) ≤ 1 - acc S x y
The defect of two coarse-grained measurements of a strategy is at most the rejection probability whenever acceptance forces the coarse-grained outcomes to agree.
theorem
MIPRE.LIDT.Bridge.pointMeasB_eq
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
:
((toProjStrat S).pointMeasurementB u).toSubMeas = MIPStarRE.LDT.postprocess (toProjMeas S.PB (Question.point (decP u))).toSubMeas codedValue
The point measurement of player B at a coded point, in coarse-grained form.
theorem
MIPRE.LIDT.Bridge.pointMeasA_eq
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
:
((toProjStrat S).pointMeasurementA u).toSubMeas = MIPStarRE.LDT.postprocess (toProjMeas S.PA (Question.point (decP u))).toSubMeas codedValue
The point measurement of player A at a coded point, in coarse-grained form.
theorem
MIPRE.LIDT.Bridge.axisMeasA_zero_eq
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
(i : Fin m)
:
(MIPStarRE.LDT.postprocess ((toProjStrat S).axisParallelMeasurementA { base := u, direction := i }).toSubMeas
fun (x : MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) = MIPStarRE.LDT.postprocess (toProjMeas S.PA (Question.axisLine (Line.through (decP u) (Pi.single i 1)))).toSubMeas
fun (a : Answer F m d) => enc (Polynomial.eval (decP u i) (axisPolyOf a))
The axis-parallel line measurement of player A evaluated at the coded parameter 0,
in coarse-grained form.
theorem
MIPRE.LIDT.Bridge.axisMeasB_zero_eq
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
(i : Fin m)
:
(MIPStarRE.LDT.postprocess ((toProjStrat S).axisParallelMeasurementB { base := u, direction := i }).toSubMeas
fun (x : MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) = MIPStarRE.LDT.postprocess (toProjMeas S.PB (Question.axisLine (Line.through (decP u) (Pi.single i 1)))).toSubMeas
fun (a : Answer F m d) => enc (Polynomial.eval (decP u i) (axisPolyOf a))
theorem
MIPRE.LIDT.Bridge.diagMeas_zero_eq
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
{n : Type u_2}
[Fintype n]
[DecidableEq n]
(P : ProjectiveMeasurement (Question F m) (Answer F m d) (Matrix n n ℂ))
(ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d))
:
(MIPStarRE.LDT.postprocess (diagMeas P ℓ).toSubMeas fun (x : MIPStarRE.LDT.DiagonalLinePolynomial (lidtParams F m d)) =>
x.toFun MIPStarRE.LDT.zeroCoord) = MIPStarRE.LDT.postprocess (toProjMeas P (Question.diagLine (Line.through (decP ℓ.base) (decP ℓ.direction)))).toSubMeas
fun (a : Answer F m d) =>
enc (Polynomial.eval ((Line.through (decP ℓ.base) (decP ℓ.direction)).param (decP ℓ.base)) (diagPolyOf a))
The diagonal line measurement of a player evaluated at the coded parameter 0, in
coarse-grained form: the line answer is read at the parameter of the base point.
theorem
MIPRE.LIDT.Bridge.accepts_axisLine_point
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
(ℓ : Line F m)
(x : Point F m)
(a b : Answer F m d)
:
accepts F m d (Question.axisLine ℓ) (Question.point x) a b = true ↔ ∃ (c : LinePoly F d) (v : F), a = Answer.axisPoly c ∧ b = Answer.value v ∧ ℓ.Mem x ∧ c.eval (ℓ.param x) = v
Acceptance for an axis-parallel line question to A and a point question to B.
theorem
MIPRE.LIDT.Bridge.accepts_point_axisLine
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
(ℓ : Line F m)
(x : Point F m)
(a b : Answer F m d)
:
accepts F m d (Question.point x) (Question.axisLine ℓ) a b = true ↔ ∃ (v : F) (c : LinePoly F d), a = Answer.value v ∧ b = Answer.axisPoly c ∧ ℓ.Mem x ∧ c.eval (ℓ.param x) = v
theorem
MIPRE.LIDT.Bridge.accepts_point_point
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
(x y : Point F m)
(a b : Answer F m d)
:
accepts F m d (Question.point x) (Question.point y) a b = true ↔ ∃ (v : F) (w : F), a = Answer.value v ∧ b = Answer.value w ∧ x = y ∧ v = w
theorem
MIPRE.LIDT.Bridge.accepts_diagLine_point
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
(ℓ : Line F m)
(x : Point F m)
(a b : Answer F m d)
:
accepts F m d (Question.diagLine ℓ) (Question.point x) a b = true ↔ ∃ (c : LinePoly F (m * d)) (v : F), a = Answer.diagPoly c ∧ b = Answer.value v ∧ ℓ.Mem x ∧ c.eval (ℓ.param x) = v
theorem
MIPRE.LIDT.Bridge.accepts_point_diagLine
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
(ℓ : Line F m)
(x : Point F m)
(a b : Answer F m d)
:
accepts F m d (Question.point x) (Question.diagLine ℓ) a b = true ↔ ∃ (v : F) (c : LinePoly F (m * d)), a = Answer.value v ∧ b = Answer.diagPoly c ∧ ℓ.Mem x ∧ c.eval (ℓ.param x) = v
theorem
MIPRE.LIDT.Bridge.axisA_defect_le
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
(i : Fin m)
:
MIPStarRE.LDT.qBipartiteConsDefect (toProjStrat S).state
(MIPStarRE.LDT.postprocess ((toProjStrat S).axisParallelMeasurementA { base := u, direction := i }).toSubMeas
fun (x : MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord)
((toProjStrat S).pointMeasurementB u).toSubMeas ≤ 1 - acc S (Question.axisLine (Line.through (decP u) (Pi.single i 1))) (Question.point (decP u))
Axis-parallel lines test, line to A.
theorem
MIPRE.LIDT.Bridge.axisB_defect_le
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
(i : Fin m)
:
MIPStarRE.LDT.qBipartiteConsDefect (toProjStrat S).state ((toProjStrat S).pointMeasurementA u).toSubMeas
(MIPStarRE.LDT.postprocess ((toProjStrat S).axisParallelMeasurementB { base := u, direction := i }).toSubMeas
fun (x : MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) ≤ 1 - acc S (Question.point (decP u)) (Question.axisLine (Line.through (decP u) (Pi.single i 1)))
Axis-parallel lines test, line to B.
theorem
MIPRE.LIDT.Bridge.point_defect_le
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(u : MIPStarRE.LDT.Point (lidtParams F m d))
:
MIPStarRE.LDT.qBipartiteConsDefect (toProjStrat S).state ((toProjStrat S).pointMeasurementA u).toSubMeas
((toProjStrat S).pointMeasurementB u).toSubMeas ≤ 1 - acc S (Question.point (decP u)) (Question.point (decP u))
Self-consistency test.
theorem
MIPRE.LIDT.Bridge.diagA_defect_le
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d))
:
MIPStarRE.LDT.qBipartiteConsDefect (toProjStrat S).state
(MIPStarRE.LDT.postprocess ((toProjStrat S).diagonalMeasurementA ℓ).toSubMeas
fun (x : MIPStarRE.LDT.DiagonalLinePolynomial (lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord)
((toProjStrat S).pointMeasurementB ℓ.base).toSubMeas ≤ 1 - acc S (Question.diagLine (Line.through (decP ℓ.base) (decP ℓ.direction))) (Question.point (decP ℓ.base))
Diagonal lines test, line to A.
theorem
MIPRE.LIDT.Bridge.diagB_defect_le
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
(ℓ : MIPStarRE.LDT.DiagonalLine (lidtParams F m d))
:
MIPStarRE.LDT.qBipartiteConsDefect (toProjStrat S).state ((toProjStrat S).pointMeasurementA ℓ.base).toSubMeas
(MIPStarRE.LDT.postprocess ((toProjStrat S).diagonalMeasurementB ℓ).toSubMeas
fun (x : MIPStarRE.LDT.DiagonalLinePolynomial (lidtParams F m d)) => x.toFun MIPStarRE.LDT.zeroCoord) ≤ 1 - acc S (Question.point (decP ℓ.base)) (Question.diagLine (Line.through (decP ℓ.base) (decP ℓ.direction)))
Diagonal lines test, line to B.
theorem
MIPRE.LIDT.Bridge.decP_extendLam
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(j : Fin m)
(v : Fin (↑j + 1) → F)
:
(decP fun (k : Fin m) => if h : ↑k ≤ ↑j then enc (v ⟨↑k, ⋯⟩) else MIPStarRE.LDT.zeroCoord) = Sample.extend v
The decoded extension of a restricted direction, as sampled in
lowIndividualDegreeFailureProbability.
The bound #
theorem
MIPRE.LIDT.Bridge.sum_fin_fun
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(j : Fin m)
(g : (Fin (↑j + 1) → MIPStarRE.LDT.Fq (lidtParams F m d)) → ℝ)
:
∑ v' : Fin (↑j + 1) → MIPStarRE.LDT.Fq (lidtParams F m d), g v' = ∑ v : Fin (↑j + 1) → F, g fun (k : Fin (↑j + 1)) => enc (v k)
Reindexing a sum over coded restricted directions.
noncomputable def
MIPRE.LIDT.Bridge.mdef
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
:
The MIPStarRE consistency defect of the branch of a sample of our game.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.LIDT.Bridge.failure_eq_sum
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
:
The MIPStarRE failure probability is the weighted sum of the branch defects over our samples.
theorem
MIPRE.LIDT.Bridge.failure_le
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
{m d : ℕ}
[NeZero m]
(S : TensorProductStrategy (lidtGame F m d))
:
The MIPStarRE failure probability of the induced strategy is at most the rejection probability of the strategy in the game.