Approximate linearity gives exact linearity #
Blueprint thm:linearity, the quantum linearity test. A family of observables
{O^u}_{u in F_q^n} that is approximately linear --- O^u O^{u'} close to O^{u + u'} on
average, in the state-dependent distance --- is close on average to a family that is exactly
linear, after adjoining an ancilla register to one player.
The paper imports this from Natarajan--Vidick; it is proved here. The route is the one the blueprint's proof text names, and every step of it is already in this repository:
- Parseval. The Fourier transform
A_e = |V|^{-1} sum_a (-1)^{<a,e>} O^aof the family against the characters of the trace form hassum_e A_e^2 = |V|^{-1} sum_a (O^a)^2 = Idwhenever eachO^ais an involution. So{A_e^2}is a POVM --- exactly, with no appeal to the approximate linearity, which is the one surprise of the argument. - Naimark.
exists_projective_dilationdilates that POVM to a projective measurement{P_e}ond x V, compressed back by the isometry that pads with the ancilla state|0>. - Inversion.
L^u = sum_e (-1)^{<u,e>} P_eis then exactly linear ---L^u L^{u'} = L^{u+u'}andL^0 = Id--- because theP_eare mutually orthogonal projections, and its compression issum_e (-1)^{<u,e>} A_e^2, which the same character sum identifies with|V|^{-1} sum_a O^a O^{a+u}. - The estimate. That average is where the hypothesis enters, and it enters once:
|V|^{-2} sum_{a,b} <psi| O^a O^b O^{a+b} |psi>is the hypothesis written out, so the closeness ofL^utoO^uon the extended state carries the samedelta, with no square root and no loss in the exponent.
The one thing to watch is which distance the hypothesis is in. It is the state-dependent one of
def:state-distance --- not the Hilbert--Schmidt distance of thm:gowers-hatami --- so this is
not Gowers--Hatami with a different normalization; the exact-POVM step above replaces the
approximate-representation machinery entirely.
The Fourier transform of a family of operators #
The Fourier transform of a family of operators indexed by V = F_q^n, against the
characters of the trace form. This is MIPRE.Weyl.proj with the index group decoupled from the
space the operators act on, and with no group law assumed.
Equations
- MIPRE.fourierOf O e = (↑(Fintype.card (n → F)))⁻¹ • ∑ a : n → F, MIPRE.sgn (MIPRE.Weyl.trDot a e) • O a
Instances For
The character sum that carries the whole argument. Summing the squares of the Fourier
coefficients against a character collapses the double sum to a single one: only the pairs with
b = a + u survive.
Parseval. The squares of the Fourier coefficients of a family of involutions form a POVM --- exactly, with no appeal to any approximate linearity.
The two-field transform of a product family factorizes. The combined measurement of a pair of parameters is the product of the two one-parameter measurements --- with no hypothesis, the double average simply splitting.
Parseval for a family of operators against a state. The transform is an isometry up to
the normalization, so an average bound on the family is a summed bound on the transform and
conversely. This is the dictionary between an F_q-valued measurement and its binary
observables.
The exactly linear family #
The exactly linear family, on the extended space. The Fourier transform of the family is
dilated to a projective measurement on d x V (exists_projective_dilation), and inverting the
transform on the dilation gives a family that is exactly linear: L^u L^{u'} = L^{u + u'}, with
the identity at 0. Its compression to the |0>-slice is the average
|V|^{-1} sum_a O^a O^{a+u}, which is what the closeness estimate compares with O^u.
The whole family is dilated by one isometry, question-independent, which is what lets the estimate be taken against a single state.
Adjoining an ancilla to one party #
The one-sided extension of a state: an ancilla register in the fixed state |a₀⟩,
adjoined to the first party only. expVec splits an ancilla pair between the two parties;
this is the asymmetric extension thm:linearity needs, the exactly linear observables living on
the first party's enlarged space and the second party untouched.
Equations
- MIPRE.extVecA ψ a₀ = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (MIPRE.ancillaEmbed dA a₀) 1).mulVec ψ
Instances For
The extension does not change the norm: the padding is an isometry.
An operator with an inert ancilla commutes with the padding isometry.
The same, on the other side of the isometry.
Compressing a product whose right factor has an inert ancilla.
Compressing a product whose left factor has an inert ancilla.
The conjugation identity: a quadratic form on the extended state is the quadratic form of the compressed operator on the original one.
The distance between two unitaries, as a quadratic form #
Expanding a squared distance. For A and B with AᴴA = BᴴB = 1 --- observables, or
products of them --- the state-dependent squared distance is 2 minus the two orders of the
overlap. Keeping both orders rather than combining them into a real part is what lets the
linearity estimate be matched term by term against its hypothesis.
The theorem #
A product of two involutions is unitary, which is all the expansion of the hypothesis's squared distance needs.
thm:linearity. A family of observables that is approximately linear on average is, after
adjoining an ancilla register to the first party, exactly linear --- a representation of F_q^n
by commuting involutions, with the identity at 0 --- and close to the original family, with the
same average error: the linearity defect is transported, not merely bounded.