Projective strategies in a bipartite model #
The soundness analysis of answer reduction is written for strategies: it restricts one to a copy
of the low-degree test, extracts polynomial measurements from the pieces, and decodes a strategy
for the input verifier's game from them. Phase 3 of planning/mipco-track.md writes it once, for
a projective strategy in a bipartite model (BipartiteModel.ProjStrat): for each question a
projective measurement in the player's algebra, on the model's state. It is TensorProductStrategy
with the tensor-product model replaced by any bipartite model, and carries the same operations —
the value, the conditional failures, playing a strategy on another game through maps of the
questions and the answers (ProjStrat.adapt), relabelling along equivalences
(ProjStrat.relabel) — each a single line over the model-level statements of
MIPRE/Foundations/GameAdapt.lean. The inconsistency of two families of measurements
(BipartiteModel.inconsistency), the error measure of the low-individual-degree test's
conclusions, is here too.
The two models the analysis is read in:
- tensor-product: a
TensorProductStrategyis a projective strategy in its tensor-product model (TensorProductStrategy.toModel, of the same value), and conversely a projective strategy in the tensor-product model of a state onFin a × Fin bis aTensorProductStrategy(BipartiteModel.ProjStrat.toTensor, of the same value); - commuting-operator:
ω_cois approached by projective strategies in the model of a commuting-operator strategy (exists_projStrat_lt_commutingOperatorValue), and the value of a projective strategy in a model on a Hilbert space is at mostω_co(BipartiteModel.ProjStrat.value_le_commutingOperatorValue).
ValueModel.Dominates ω M says that every projective strategy of M has value at most ω;
both models are dominated by their value (ValueModel.tensor_dominates,
ValueModel.commuting_dominates). So a model-level theorem — a projective strategy of value at
least 1 - ε for one game gives a projective strategy of value at least 1 - f(ε) for another,
in the same model — bounds the second game's value in both values.
Coarse-grainings of POVMs in a ⋆-algebra #
Relabelling twice is relabelling once: the level sets of g ∘ f are the unions of the
level sets of f along the level sets of g.
Relabelling along the identity changes nothing.
The coarse-graining of a projective measurement is projective.
Coarse-graining a matrix POVM is coarse-graining it in the matrix algebra.
Projective strategies #
A projective strategy in a bipartite model for the game G: for each question a
projective measurement in the player's algebra, on the model's state, which is a unit vector.
TensorProductStrategy is the case of the tensor-product model
(TensorProductStrategy.toModel); a projective commuting-operator strategy is one in its own
model (exists_projStrat_lt_commutingOperatorValue).
- PA : X → POVMIn A 𝒜
The first player's measurement at each question.
- PB : Y → POVMIn B ℬ
The second player's measurement at each question.
The first player's measurements are projective.
The second player's measurements are projective.
The model's state is a unit vector.
Instances For
Two games with the same distribution and the same decision predicate give every family of measurements the same value.
The value of a projective strategy: the value of its measurements in the model.
Instances For
The probability that the strategy is rejected, given the question pair (x, y).
Instances For
The failure probability, decomposed by question pair.
Playing a strategy on another game #
Play S on G', through a map qA, qB of G''s questions into G's and a
coarse-graining rA, rB of G's answers into G''s that may depend on the question: the
measurement at a question x' of G' is the one S uses at qA x', with its outcomes merged
along rA x'. A coarse-graining of a projective measurement is projective.
Equations
- S.adapt G' qA qB rA rB = { PA := fun (x' : X') => MIPRE.POVMIn.map (rA x') (S.PA (qA x')), PB := fun (y' : Y') => MIPRE.POVMIn.map (rB y') (S.PB (qB y')), projA := ⋯, projB := ⋯, ψ_unit := ⋯ }
Instances For
The adapted strategy fails no more often, at a question pair where every tuple G
accepts is still accepted after coarse-graining.
Relabel a strategy along equivalences of the questions and the answers.
Equations
Instances For
Relabelling keeps the value, when the equivalences carry G' onto G.
Restrict a strategy to other questions: the same measurements, asked at the images of the new questions; the answers are kept.
Equations
Instances For
The inconsistency of two families of measurements #
The inconsistency of the first player's family P and the second player's Q on the
index weighted by μ: the weight of the outcome pairs that differ. The matrix inconsistency
is its tensor-product instance (inconsistency_eq_tensor).
Equations
Instances For
The inconsistency is the weighted disagreement.
On a uniform index, the inconsistency is the average disagreement.
A bound on the inconsistency on a uniform index is a bound on the summed disagreement.
On a one-point index, the inconsistency is the disagreement.
The matrix inconsistency is the inconsistency in the tensor-product model.
The tensor-product model #
A tensor-product strategy is a projective strategy in its tensor-product model: its measurements as POVMs in the two matrix algebras.
Equations
Instances For
A projective strategy in the tensor-product model of a state on Fin a × Fin b is a
tensor-product strategy, on the same state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The commuting-operator model #
The value of a projective strategy in a model on a Hilbert space is at most ω_co: it is
a commuting-operator strategy (BipartiteModel.toCommuting).
ω_co is approached by projective strategies in the models of commuting-operator
strategies (exists_isPVMIn_lt_povmValue).
Value models dominating a bipartite model #
The value model dominates the projective strategies of a bipartite model: each has value at most the value of its game.
Equations
Instances For
ω_co dominates every bipartite model on a Hilbert space.