Parseval for the character transform

The combining stage of the Pauli appendix moves between two descriptions of the same data: an F_q-valued measurement {P_a} and its binary observables O^r = sum_a (-1)^{tr(ar)} P_a, one for each r in F_q. The two are Fourier transforms of each other, and what the estimates need is that the transform is an isometry: a bound on the observables, averaged over r, is a bound on the measurement elements, summed over a, and conversely.

This file is that dictionary, for vectors and for families of matrices applied to a state:

• fourierVec is the transform of a family of vectors indexed by V = F_q^n, against the characters of the trace form, and sum_norm_fourierVec_sq is Parseval --- an identity, not an estimate;
• trObs is the observable of an F_q-indexed family at a parameter r, trObs_fourier inverts it, and sum_stateSqNorm_eq_avg_trObs is Parseval in the form the appendix uses: the sum over outcomes of the squared state-norms of the elements is the average over r of the squared state-norms of the observables.

The one-field character orthogonality it all rests on is MIPRE.Weyl.sum_sgn_trMul.

The transform of a family of vectors

noncomputable def MIPRE.fourierVec {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {N : Type u_3} (T : (n → F) → N → ℂ) (e : n → F) : N → ℂ

The character transform of a family of vectors indexed by V = F_q^n.

Equations

• MIPRE.fourierVec T e = (↑(Fintype.card (n → F)))⁻¹ • ∑ a : n → F, MIPRE.sgn (MIPRE.Weyl.trDot a e) • T a

noncomputable def MIPRE.fourierVecRaw {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {N : Type u_3} (T : (n → F) → N → ℂ) (e : n → F) : N → ℂ

The unnormalized transform: the same sum without the 1/|V|.

Equations

• MIPRE.fourierVecRaw T e = ∑ a : n → F, MIPRE.sgn (MIPRE.Weyl.trDot a e) • T a

theorem MIPRE.fourierVec_eq_smul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {N : Type u_3} [Fintype N] [DecidableEq N] (T : (n → F) → N → ℂ) (e : n → F) : fourierVec T e = (↑(Fintype.card (n → F)))⁻¹ • fourierVecRaw T e

theorem MIPRE.sum_dotProduct_fourierVecRaw {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {N : Type u_3} [Fintype N] [DecidableEq N] (T : (n → F) → N → ℂ) : ∑ e : n → F, star (fourierVecRaw T e) ⬝ᵥ fourierVecRaw T e = ↑(Fintype.card (n → F)) * ∑ a : n → F, star (T a) ⬝ᵥ T a

The character sum, on the sesquilinear form. Only the diagonal survives.

theorem MIPRE.dotProduct_star_self {N : Type u_3} [Fintype N] [DecidableEq N] (v : N → ℂ) : star v ⬝ᵥ v = ↑(‖evec v‖ ^ 2)

The sesquilinear form of a vector with itself is its squared norm, as a complex number.

theorem MIPRE.sum_norm_fourierVecRaw_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {N : Type u_3} [Fintype N] [DecidableEq N] (T : (n → F) → N → ℂ) : ∑ e : n → F, ‖evec (fourierVecRaw T e)‖ ^ 2 = ↑(Fintype.card (n → F)) * ∑ a : n → F, ‖evec (T a)‖ ^ 2

Parseval for the character transform. The transform is an isometry up to the normalization: the sum of the squared norms of the transform is the average of the squared norms of the family. No hypothesis on the family at all.

theorem MIPRE.sum_norm_fourierVec_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {N : Type u_3} [Fintype N] [DecidableEq N] (T : (n → F) → N → ℂ) : ∑ e : n → F, ‖evec (fourierVec T e)‖ ^ 2 = (↑(Fintype.card (n → F)))⁻¹ * ∑ a : n → F, ‖evec (T a)‖ ^ 2

The one-field transform, and its inverse

The appendix's other direction: an F_q-valued family P has binary observables O^r = sum_a (-1)^{tr(ar)} P_a, and P is recovered from O by the same transform, averaged.

noncomputable def MIPRE.trObs {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {N : Type u_3} (P : F → Matrix N N ℂ) (r : F) : Matrix N N ℂ

The binary observable of an F_q-indexed family of operators at the probe r.

Equations

• MIPRE.trObs P r = ∑ a : F, MIPRE.sgn ((Algebra.trace (ZMod 2) F) (a * r)) • P a

noncomputable def MIPRE.trFourier {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {N : Type u_3} (A : F → Matrix N N ℂ) (a : F) : Matrix N N ℂ

The transform back: the a-th element recovered from the observables.

Equations

• MIPRE.trFourier A a = (↑(Fintype.card F))⁻¹ • ∑ r : F, MIPRE.sgn ((Algebra.trace (ZMod 2) F) (a * r)) • A r

theorem MIPRE.trFourier_trObs {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {N : Type u_3} [Fintype N] [DecidableEq N] (P : F → Matrix N N ℂ) (a : F) : trFourier (trObs P) a = P a

Fourier inversion over one copy of the field.

Coarse-grainings and the transform

A measurement is usually presented as a POVM whose outcomes are then read by a function; the transform has to see through that reading. Both lemmas below are the same regrouping of a sum along the fibres of the reading.

theorem MIPRE.trObs_map {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {A : Type u_4} [Fintype A] [DecidableEq A] {dA : Type u_5} [Fintype dA] [DecidableEq dA] (P : POVM A dA) (f : A → F) (r : F) : trObs (fun (a : F) => ↑((POVM.map f P).mats a)) r = ∑ x : A, sgn ((Algebra.trace (ZMod 2) F) (f x * r)) • ↑(P.mats x)

The one-field transform sees through a coarse-graining.

The two-field transform of a product

The combined measurement is indexed by a pair (a, b), and the family it transforms is a product of one operator depending on r and one depending on s. The transform factorizes, which is why the combined measurement is the product of the two marginals whenever the two commute.

def MIPRE.pairVec {F : Type u_1} (r s : F) : Fin 2 → F

The pair (r, s) as a vector of F_q^2.

Equations

• MIPRE.pairVec r s i = if i = 0 then r else s

@[simp]

theorem MIPRE.pairVec_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] (r s : F) : pairVec r s 0 = r

@[simp]

theorem MIPRE.pairVec_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] (r s : F) : pairVec r s 1 = s

theorem MIPRE.trDot_pairVec {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] (r s a b : F) : Weyl.trDot (pairVec r s) (pairVec a b) = (Algebra.trace (ZMod 2) F) (a * r) + (Algebra.trace (ZMod 2) F) (b * s)

theorem MIPRE.sum_pairVec {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {M : Type u_6} [AddCommMonoid M] (f : (Fin 2 → F) → M) : ∑ v : Fin 2 → F, f v = ∑ r : F, ∑ s : F, f (pairVec r s)

theorem MIPRE.sum_prod_eq_sum_pairVec {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {M : Type u_6} [AddCommMonoid M] (f : F → F → M) : ∑ p : F × F, f p.1 p.2 = ∑ v : Fin 2 → F, f (v 0) (v 1)

A sum over pairs is a sum over F_q^2.

Parseval over one copy of the field, and over two

The combining stage coarse-grains an F_q x F_q-valued measurement by the linear form (a, b) |-> alpha a + beta b, and the fibres have q elements -- so a per-fibre triangle inequality would cost a factor q. Parseval is what avoids that, and it is needed in three shapes: over F_q (to turn the sum over fibres into an average over one probe), over F_q x F_q (to turn that average back into a sum over outcome pairs), and the cancellation of the zero probe.

noncomputable def MIPRE.trVecRaw {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {N : Type u_3} (T : F → N → ℂ) (r : F) : N → ℂ

The unnormalized character transform of a family of vectors indexed by F_q itself.

Equations

• MIPRE.trVecRaw T r = ∑ c : F, MIPRE.sgn ((Algebra.trace (ZMod 2) F) (c * r)) • T c

theorem MIPRE.sum_dotProduct_trVecRaw {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {N : Type u_3} [Fintype N] [DecidableEq N] (T : F → N → ℂ) : ∑ r : F, star (trVecRaw T r) ⬝ᵥ trVecRaw T r = ↑(Fintype.card F) * ∑ c : F, star (T c) ⬝ᵥ T c

theorem MIPRE.sum_norm_trVecRaw_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {N : Type u_3} [Fintype N] [DecidableEq N] (T : F → N → ℂ) : ∑ r : F, ‖evec (trVecRaw T r)‖ ^ 2 = ↑(Fintype.card F) * ∑ c : F, ‖evec (T c)‖ ^ 2

Parseval over one copy of the field.

theorem MIPRE.sum_norm_char_two_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {N : Type u_3} [Fintype N] [DecidableEq N] (T : F × F → N → ℂ) : ∑ q : F × F, ‖evec (∑ p : F × F, sgn ((Algebra.trace (ZMod 2) F) (q.1 * p.1) + (Algebra.trace (ZMod 2) F) (q.2 * p.2)) • T p)‖ ^ 2 = ↑(Fintype.card F) * ↑(Fintype.card F) * ∑ p : F × F, ‖evec (T p)‖ ^ 2

Parseval over two copies of the field, in the product-indexed shape the combining stage uses.

Coarse-graining by a linear form

theorem MIPRE.sum_avg_norm_fibre_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {N : Type u_3} [Fintype N] [DecidableEq N] (U : F × F → N → ℂ) (hU : ∑ p : F × F, U p = 0) : ∑ ab : F × F, (↑(Fintype.card F))⁻¹ * (↑(Fintype.card F))⁻¹ * ∑ c : F, ‖evec (∑ p : F × F with ab.1 * p.1 + ab.2 * p.2 = c, U p)‖ ^ 2 = (1 - (↑(Fintype.card F))⁻¹) * ∑ p : F × F, ‖evec (U p)‖ ^ 2

Parseval for a coarse-graining by a linear form. A family of vectors indexed by F_q x F_q that sums to zero has, on average over (alpha, beta) uniform, fibre sums under (a, b) |-> alpha a + beta b whose total squared norm is 1 - 1/q times the family's own. In particular it is at most the family's: the fibres have q elements, and a per-fibre triangle inequality would cost exactly that factor, which this avoids.

The zero-sum hypothesis is what kills the r = 0 character; without it the statement is false (take U supported on one point).