Playing a strategy for one game as a strategy for another #
MIPRE.Foundations.GameTransport compares games that share their question alphabets and their
distribution. This file drops both assumptions, which is what a reduction between two
genuinely different games needs: given a strategy S for G, a map qA of the target game's
questions into G's and a coarse-graining rA of G's answers into the target's, S.adapt
plays S through them.
The conditional success probability #
Everything is organized around succAt S x y, the probability that S is accepted given the
question pair (x, y), and its complement failAt. The value is the μ-average of succAt
(value_eq_sum_succAt), so
1 - S.value = ∑ x y, μ x y * failAt S x y (one_sub_value_eq_sum_failAt),
which is the form a reduction compares across two games: an inequality between failure probabilities, each weighted by its own game's distribution.
What the adapter costs #
failAt_adapt_le says the adapted strategy fails no more often at (x', y') than S does at
(qA x', qB y'), provided every tuple G accepts is still accepted after coarse-graining
(hD). The summed statements ask hD only where G'.μ is nonzero, and that is not a
convenience: a question pair outside the target's support may well be one the target rejects
and the source accepts --- for the seeded CL test, a pair of two line questions, which the
canonical-line test has no subtest for --- so the unrestricted hypothesis would be false. Summing, the price is entirely in the distributions: one_sub_value_adapt_le asks that
the push-forward of G''s distribution along (qA, qB) be dominated by C times G's, and
concludes 1 - (S.adapt …).value ≤ C * (1 - S.value).
Derandomization #
A reduction usually cannot choose the question map canonically: the target's question is
typically a coarser object than G's — a line rather than a seeded description of a line —
so one has to pick a preimage, and for any fixed choice the push-forward bound is off by the
size of the fibre. exists_one_sub_value_adapt_le is the averaged form. It asks only that the
push-forward bound hold on average over a finite family of question maps, and returns one
member of the family achieving the conclusion. That is the "choose the best seed" step, and the
averaging is exactly where the fibre size is paid back.
In a bipartite model #
A strategy in a bipartite model is a POVM family in each player's algebra and its value is
BipartiteModel.povmValue; the adapted strategy is fun x' => (MA (qA x')).map (rA x'), and every
statement above is proved once for it (BipartiteModel.condWin_adapt,
BipartiteModel.one_sub_povmValue_adapt_le, ...). A tensor-product strategy is the strategy of its
measurements in its tensor-product model (TensorProductStrategy.value_eq_tensor_povmValue), and
its adapted strategy the model's (TensorProductStrategy.value_adapt), so the statements about
TensorProductStrategy.adapt are instances.
A double sum over the fibres of two coarse-grainings is the double sum.
Question-dependent merging of outcomes #
Merge the outcomes of P along a coarse-graining that may depend on the question, while
reindexing the questions. GameTransport's merge is the case of a coarse-graining that does
not depend on the question; a reduction generally needs the dependence, because how an answer
must be converted can depend on which question was asked --- the reparametrization of a line
answer depends on the line.
Equations
Instances For
Playing a strategy through maps, in a bipartite model #
A strategy in a bipartite model is a family of POVMs in each player's algebra, and its value is
BipartiteModel.povmValue (TensorProductStrategy.value_eq_povmValue and
povmValue_eq_tensor in the tensor-product model; CommutingOperatorStrategy.value_eq_povmValue
in the commuting-operator model). Playing it on another game through a map of questions and a
coarse-graining of answers is fun x' => (MA (qA x')).map (rA x'), and everything below is
proved once for it; the statements about TensorProductStrategy.adapt further down are its
instances.
The adapted conditional acceptance, as a sum over the original answers: the coarse-graining disappears into the decision predicate.
The adapter does not lose acceptance where every tuple G accepts is still accepted
after coarse-graining.
Equivalently: the adapted strategy fails no more often.
Relabeling a strategy along equivalences keeps its value: the model form of
TensorProductStrategy.value_relabel, and the content of ValueModel.eq_of_equiv for a strategy
in a model.
The failure of the adapted strategy, bounded by G's conditional failures weighted by the
push-forward of G''s distribution.
The cost of the adapter. If the push-forward of G''s question distribution along
(qA, qB) is dominated by C times G's, the adapted strategy's failure is at most C times
the original's.
The summed form of one_sub_povmValue_adapt_le over a finite family of question maps,
when the push-forward bound holds on average.
The averaged form of one_sub_povmValue_adapt_le: some member of a finite family of
question maps achieves the conclusion when the push-forward bound holds on average.
Born-rule probabilities and the conditional success probability #
The Born-rule probability that S answers (a, b) to the question pair (x, y).
Equations
Instances For
The Born probability of a strategy is that of its tensor-product model.
The probability that S is accepted, given the question pair (x, y).
Instances For
The probability that S is rejected, given the question pair (x, y).
Instances For
The conditional success probability is that of the tensor-product model.
The value of a strategy is the value of its measurements in its tensor-product model.
The adapted strategy #
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'.
Equations
Instances For
The merged measurement is the coarse-graining of the original, as a POVM in the matrix algebra.
The adapted strategy is the model's adapted strategy: its value is the value, in the
tensor-product model of S, of the coarse-grained measurements.
The adapter does not lose acceptance. If every tuple G accepts at (qA x', qB y') is
still accepted by G' at (x', y') after coarse-graining, the adapted strategy succeeds at
least as often there.
Equivalently: the adapted strategy fails no more often.
The cost of the adapter is the push-forward of the distribution #
The cost of the adapter. If the push-forward of G''s question distribution along
(qA, qB) is dominated by C times G's, the adapted strategy's failure is at most C times
S's.
Derandomization #
The averaged form of one_sub_value_adapt_le. The push-forward bound need only hold on
average over a finite family of question maps; some member of the family then achieves the
conclusion. This is how a reduction that must choose a preimage of each target question pays
back the size of the fibre.