The mass at non-multilinear outcomes (lem:qld-exact-paulis, the approximate half) #
The Pauli construction of MIPRE/Background/QLD/ExactPauli.lean reads an outcome g of the
simultaneous measurement through the multilinear interpolant of its values on the boolean cube,
Coded(g) ยท ind_m(u), rather than through g(u) itself. The two agree exactly when g is
multilinear and not otherwise, so the construction is consistent with the strategy's point
measurement up to the mass the simultaneous measurement puts on non-multilinear outcomes.
That mass is what the paper's lem:qld-construct-the-paulis bounds, in an argument it repaired
twice. The repair is to compare the outcome not with the point measurement --- whose label depends
on the sampled point --- but with a projective family indexed by cube data, which does not.
Then the point is independent of the operators, and Schwartz--Zippel applies in the direction it
is true in: two distinct polynomials of total degree md agree on at most an md/q fraction.
This file is the aggregation step, stated so that its two inputs are visible: a lower bound on the agreement with the cube-data family, and a uniform bound on the probability that a bad outcome agrees with any one of its labels.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The pair measurement is a
SimulPair M S K ฮน ฮด of a projective strategy S of a bipartite model M: its marginals are POVMs
in K's first algebra, and the second player's expanded measurements --- the hatted point
measurement and the hatted Pauli basis measurement hatPauli, POVMs of the register model
M.reg (Anc F m) --- are read in K through the embedding ฮน. The aggregation and substitution
steps are stated in any bipartite model; the squared distance they meet is carried from the
register model to K exactly (SimulPair.normSq_stateVecB_aOp). The projectivity of the
strategy, a hypothesis of the matrix statements, is a field of S.
The aggregation step. S is a projective measurement of one player and N one of the
other, val and ev two labellings by a field element at each question, and the agreement of S
with N under matching labels is at least 1 - ฮท. If off a set ML every outcome of S matches
every label of N with probability at most c, the mass of S off ML is at most ฮท + c.
The averaged substitution estimate. Against a projective family at each question, an agreement with any family of the other player is bounded by the root of that family's average weight: Cauchy--Schwarz at each question, then Jensen for the average.
Grouping an agreement by the common label. Summing the Born probabilities of all outcome
pairs whose labels match is the same as summing the two coarse-grained measurements against each
other at each label. This is what lets the helper's agreement, which is stated at an outcome in
F_q, be read as an agreement between the polynomial-indexed marginal and a point-independent
family of the other player.
Reading a coarse-grained measurement against a family indexed by the labels is reading the original measurement against the family at its own label.
Multilinear outcomes, and Schwartz--Zippel against every cube datum at once #
A multilinear outcome: every monomial has each exponent at most one, so the outcome is its own multilinear interpolant.
Equations
Instances For
A non-multilinear outcome has an individual degree above one, so it is distinct from the interpolant of every cube datum.
Schwartz--Zippel, in the direction the repair needs: a non-multilinear outcome agrees with
the interpolant of a cube datum at a uniform point with probability at most md/q, and the bound
does not depend on the datum.
Outcomes the Pauli construction reads correctly #
mTilde labels the outcome g not by g(u) but by \coded(g) . ind_m(u), the value at u of
the low-degree encoding of g's values on the boolean cube. The two agree exactly on the outcomes
that are their own encoding, and the appendix's repair is to bound the mass off that set. IsML
is the syntactic version of the set; IsInterp is the semantic one, and it is the one the
construction needs, because it is also what makes Schwartz--Zippel apply off it.
The cube data of an outcome: its values on {0,1}^m, the paper's \coded(g).
Equations
- MIPRE.QLD.cubeData g y = g.eval (MIPRE.LowDegree.pt y)
Instances For
An outcome that is the low-degree encoding of its own cube data.
Equations
Instances For
The cube data of an encoding is the data it encodes.
So being some encoding is being one's own.
An outcome that is not an interpolant is distinct from the encoding of every cube datum, which is what makes the Schwartz--Zippel bound below uniform in the datum.
On an interpolant the construction's label is the outcome's own value, which is exactly why the substitution is free there.
Schwartz--Zippel off the interpolants, uniformly in the cube datum.
The marginal indexed by polynomials #
evalMarg reads the pair measurement's W component through its value at the sampled point, so
the family it names depends on the point. The repaired argument needs a family that does not: the
Schwartz--Zippel bound is applied to a fixed outcome operator against a point drawn afterwards.
polyMarg is that family, and evalMarg is its coarse-graining at each point.
The W marginal of a pair measurement, indexed by polynomials.
Equations
Instances For
The evaluated marginal is the polynomial marginal read at the point.
The polynomial marginal of a projective pair measurement is projective.
The mass the simultaneous measurement puts on non-multilinear outcomes #
The hatted Pauli family is projective: a product of two projective measurements, coarse grained along the sum of their outcomes.
The substitution. Replacing Bob's expanded point measurement by the point-independent
hatted Pauli family inside the helper's agreement costs sqrt (688 eps): one Cauchy--Schwarz at
each point against Alice's projective marginal, then Jensen for the average over points.
The mass off a set of outcomes, the critical step of lem:qld-construct-the-paulis.
Alice's polynomial-indexed marginal agrees, at a point sampled after the operators are fixed,
with the point-independent hatted Pauli family; if off ML an outcome can agree with any one cube
datum with probability at most c, the mass the marginal puts off ML is at most the sum of the
two errors.
The mass at non-multilinear outcomes.
The mass at outcomes that are not the encoding of their own cube data --- the form the Pauli construction consumes, since it is exactly off this set that its label differs from the outcome's own value.
The helper's agreement, regrouped by the outcome polynomial rather than by its value.
lem:qld-exact-paulis, item 1, as the agreement the appendix's chain establishes.
mTilde reads the outcome g through the value at u of the encoding of its cube data,
\coded(g) . ind_m(u), and not through g(u); expanding its definition and contracting the
generalized Pauli on the opposite party's ancilla against the strategy's point measurement turns
the agreement of mTilde with M^{(Point,W),u} into the left-hand side below. It differs from
the helper's agreement only at outcomes that are not their own encoding, where the two labels can
differ, and each term is at most the outcome's own weight; so twice the mass off the interpolants
pays for the substitution.