The state calculus of the Pauli basis test's last stages, in a model #
The soundness analysis of the Pauli basis test (MIPRE/Background/QLD/) proves a handful of
estimates about a single state vector on the way, each stated for matrices on โ^N and a vector
v : N โ โ. New in Phase 5 of planning/mipco-track.md, where that analysis is stated in a
bipartite model: their forms in a state model (MIPRE/Foundations/StateModel.lean), with the
operators in the represented algebra ๐ and the state the model's, and for a bipartite model
(MIPRE/Foundations/BipartiteModel.lean) where a player's family is meant. A matrix statement is
the model statement in StateModel.mat v or BipartiteModel.tensor ฯ.
- Orthogonal outcomes have no cross terms (
StateModel.snorm_sq_sum_orthogonal, andStateModel.snorm_sq_sum_orthogonal'with a different tail on each outcome): both areStateModel.snorm_sq_sum_proj_mulofMIPRE/Foundations/Commutation.leanfor a projective measurement. - A chain of
ndeviations costs a factorn(StateModel.sum_snorm_sq_chain_le), not the2โฟof iterating the triangle inequalityStateModel.sum_snorm_sq_triangle. - Weighting by coefficients of modulus at most one costs the size of the outcome set
(
StateModel.snorm_sq_obs_sub_le), the state-norm form oflem:qld-povm-to-obs. - Moving a quadratic form to a nearby state costs twice the operator bound times the distance
(
StateModel.abs_qform_sub_qform_le, on two vectors of the model's space throughStateModel.withState;Op.abs_qform_sub_qform_leon the operators). - Two families of total squared norm at most one are at total squared distance at most four
(
BipartiteModel.sum_stateSqNorm_sub_le_four_of_le), so in particular two projective measurements on a unit vector (BipartiteModel.sum_stateSqNorm_sub_le_four): the trivial bound of the second item ofthm:qld. - Parseval for a coarse-graining by a linear form, in any complex inner product space
(
sum_avg_norm_fibreSum_sq), from Parseval for an orthogonal family of characters (sum_norm_charSum_sq) over one copy of the field and over two (sum_norm_trSum_sq,sum_norm_trSum2_sq). It is the vector statementsum_avg_norm_fibre_sqofMIPRE/Foundations/Parseval.leanwith the vectors in any Hilbert space. In a state model it isStateModel.sum_avg_snorm_sq_fibre_eq, a family of the model's algebra summing to zero; for a player's familyBipartiteModel.sum_avg_stateSqNorm_fibre_eq(the second player's throughM.swap), and for a cross-party deviation of two families summing to one,BipartiteModel.sum_avg_xSqNorm_fibre_eq.
These replace matrix lemmas the QLD chain used before it was stated in a bipartite model (Phase 5
of planning/mipco-track.md): snorm_sq_sum_orthogonal, snorm_sq_sum_orthogonal',
sum_snorm_sq_chain_le, snorm_sq_obs_sub_le, abs_qform_sub_qform_le, and for Parseval
sum_avg_normSq_stateVecB_fibre_eq and sum_avg_xSqNorm_fibre_eq. The trivial bound replaces the
matrix bounds sum_snorm_sq_registerState_alice_le_two and _bob_le_two of the matrix thm:qld,
with the constant 4 that le_qldErr allows in place of their 2. The model form of the
triangle inequality sum_snorm_sq_triangle' was already StateModel.sum_snorm_sq_triangle.
Moving a quadratic form to a nearby vector #
Moving a quadratic form to a nearby vector costs twice the bound times the distance. The difference splits into two terms, each with the deviation on one side, and each is bounded by Cauchy--Schwarz against a vector of norm at most one.
The state calculus in a state model #
A sum of orthogonal blocks has no cross terms. If S is a projective measurement then,
for any R, the squared state norm of (โ g โ s, S g) R is the sum of those of the S g R.
The model form of the matrix snorm_sq_sum_orthogonal of QLD/Pulling.lean.
A sum of orthogonal blocks has no cross terms, even with a different tail on each. The
model form of the matrix snorm_sq_sum_orthogonal' of QLD/Chain.lean.
The triangle inequality along a chain of deviations. A chain of n steps costs a factor
n, not 2โฟ: the total deviation telescopes into the sum of the steps', and Cauchy--Schwarz
against the constant one turns the squared norm of a sum of n terms into n times the sum of
their squares. The model form of the matrix sum_snorm_sq_chain_le of QLD/Chain.lean, over any
finite set of indices (the matrix one is s = univ).
From measurement elements to weighted sums of them: weighting both families by
coefficients of modulus at most one costs a factor the size of the outcome set, by the triangle
inequality over the outcomes and then Cauchy--Schwarz against the constant one. It replaces the
matrix snorm_sq_obs_sub_le of the QLD chain (lem:qld-povm-to-obs).
Moving a quadratic form to a nearby state costs twice the bound times the distance, for
two vectors v, w of norm at most one of the model's space, each read as the state
(StateModel.withState). The model form of the matrix abs_qform_sub_qform_le of
QLD/SwapMeasure.lean.
abs_qform_sub_qform_le against the model's own state.
The trivial bound on a summed distance #
The summed squared distance of two families is at most twice the sum of their summed
squared norms: the triangle inequality through 0.
Two families each of summed squared norm at most one are at summed squared distance at most
four. This covers two POVMs on a unit vector (sum_stateSqNorm_le_one), sub-POVMs, and the
images of projective measurements under a non-unital โ-homomorphism.
Two projective measurements on a unit vector are at summed squared distance at most
four: the trivial bound of the second item of thm:qld (the second player's is this in
M.swap), in place of the bounds sum_snorm_sq_registerState_alice_le_two and _bob_le_two of
the matrix thm:qld. The matrix bound 2 uses that on the register state the honest
projector on one party is the same projector on the other; 4 needs nothing, and is what
le_qldErr asks for.
Parseval in a complex inner product space #
MIPRE/Foundations/Parseval.lean proves the character Parsevals for vectors of โ^N; the same
statements hold, with the same proof, in any complex inner product space, and that is the form a
state model needs: the vectors are ฯ(T) ฯ in the model's Hilbert space.
Parseval for an orthogonal family of characters, in any complex inner product space: if
the characters ฯ r satisfy โ_r conj(ฯ r a) ฯ r b = c ฮด_{ab}, then the transform
r โฆ โ_a ฯ r a โข T a has total squared norm c times the family's.
The one-field character sum, as an if.
The characters c โฆ (-1)^{tr(c r)} are orthogonal, with norm q.
The characters p โฆ (-1)^{tr(qโ pโ) + tr(qโ pโ)} of F_q ร F_q are orthogonal, with norm
qยฒ.
Parseval over one copy of the field, in any complex inner product space: the matrix
sum_norm_trVecRaw_sq of MIPRE/Foundations/Parseval.lean with the vectors in E.
Parseval over two copies of the field, in any complex inner product space: the matrix
sum_norm_char_two_sq of MIPRE/Foundations/Parseval.lean with the vectors in E.
Parseval for a coarse-graining by a linear form, in any complex inner product space. A
family of vectors indexed by F_q ร F_q that sums to zero has, on average over (ฮฑ, ฮฒ)
uniform, fibre sums under (a, b) โฆ ฮฑ a + ฮฒ b whose total squared norm is 1 - 1/q times the
family's own; a per-fibre triangle inequality would cost the factor q the fibres have. The
matrix sum_avg_norm_fibre_sq of MIPRE/Foundations/Parseval.lean with the vectors in E, by
the same proof; the zero-sum hypothesis kills the r = 0 character.
Parseval in a model #
Parseval over F_q for the fibre sums of a family summing to zero, in a state model: the
average over the combining coefficients of the squared state norms of the fibre sums is
(1 - 1/q) times the sum of the squared state norms of the members. sum_avg_norm_fibreSum_sq
on the vectors ฯ(E p) ฯ.
Parseval over F_q for the fibre sums of a player's family summing to zero. For the
second player's family E : F ร F โ โฌ it is the statement in M.swap, whose state norm is
โฯB(ยท) ฯโ: the model form of the matrix sum_avg_normSq_stateVecB_fibre_eq of
QLD/Products.lean, whose fibre sum ptComb E ฮฑ ฮฒ c is the one here.
Parseval over F_q for the fibre sums of a cross-party deviation: two families, one for
each player, each summing to one, coarse-grained by (a, b) โฆ ฮฑ a + ฮฒ b. The model form of the
matrix sum_avg_xSqNorm_fibre_eq of QLD/Combined.lean.