Documentation

MIPRE.Foundations.Introspection.CommutatorParseval

Parseval for commutators with linear-map readouts #

The character transform on the kernel's perpendicular identifies the outcome-summed commutator error of a linear-map measurement with the uniformly averaged error of its Pauli observables. This proves the characteristic-two form of the paper's lem:W. The identity holds on every state, with ancillary spaces and empty fibres allowed.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md) whose first player's algebra carries the register, Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ, with a register operator P acting as smulKron 1 P, and Parseval in any complex inner product space.

source
theorem MIPRE.Introspection.instCharPOfNatNat_mIPRE_1 {F : Type u_1} [Field F] [Algebra (ZMod 2) F] :
CharP F 2
source
theorem MIPRE.Introspection.linearPreimage_mem_range {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) {y : Fin n โ†’ F} (hy : y โˆˆ L.range) :
L (linearPreimage L y) = y

A chosen preimage maps to its target whenever the target lies in the range.

source
theorem MIPRE.Introspection.sum_linear_fiber_sign {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) {a b : Fin n โ†’ F} (ha : a โˆˆ L.range) (hb : b โˆˆ L.range) :
โˆ‘ v : โ†ฅ(CL.perp L.ker), sgn (Weyl.trDot (โ†‘v) (linearPreimage L a + linearPreimage L b)) = if a = b then โ†‘(Fintype.card โ†ฅ(CL.perp L.ker)) else 0

Distinct nonempty fibres have orthogonal characters on the kernel's perpendicular.

source
theorem MIPRE.Introspection.sum_norm_linearFourier_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace โ„‚ E] (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) (T : (Fin n โ†’ F) โ†’ E) (hT : โˆ€ y โˆ‰ L.range, T y = 0) :
(โ†‘(Fintype.card โ†ฅ(CL.perp L.ker)))โปยน * โˆ‘ v : โ†ฅ(CL.perp L.ker), โ€–โˆ‘ y : Fin n โ†’ F, sgn (Weyl.trDot (โ†‘v) (linearPreimage L y)) โ€ข T yโ€– ^ 2 = โˆ‘ y : Fin n โ†’ F, โ€–T yโ€– ^ 2

Parseval for vector families supported on the range of a linear map, in any complex inner product space.

source
theorem MIPRE.Introspection.linear_measurement_parseval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace โ„‚ E] (w : (Fin n โ†’ F) โ†’ Matrix (Fin n โ†’ F) (Fin n โ†’ F) โ„‚) (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) (f : Matrix (Fin n โ†’ F) (Fin n โ†’ F) โ„‚ โ†’โ‚—[โ„‚] E) :
โˆ‘ y : Fin n โ†’ F, โ€–f (Weyl.synOf w (โ‡‘L) y)โ€– ^ 2 = (โ†‘(Fintype.card โ†ฅ(CL.perp L.ker)))โปยน * โˆ‘ v : โ†ฅ(CL.perp L.ker), โ€–f (w โ†‘v)โ€– ^ 2

The readout/observable Parseval identity after any linear action on vectors.

source
def MIPRE.Introspection.commutatorAction {F : Type u_1} [Fintype F] [DecidableEq F] {n : โ„•} {๐’ž : Type u_3} {๐’œ : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮจ : BipartiteModel ๐’ž (Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) โ„ฌ) (M : Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) :
Matrix (Fin n โ†’ F) (Fin n โ†’ F) โ„‚ โ†’โ‚—[โ„‚] ฮจ.H

Commute a register operator with M and apply the result to the state of a model whose first player's algebra carries the register, Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ: a register operator P is smulKron 1 P.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.linear_measurement_commutator_parseval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {๐’ž : Type u_3} {๐’œ : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (w : (Fin n โ†’ F) โ†’ Matrix (Fin n โ†’ F) (Fin n โ†’ F) โ„‚) (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) (ฮจ : BipartiteModel ๐’ž (Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) โ„ฌ) (M : Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) :
    โˆ‘ y : Fin n โ†’ F, ฮจ.stateSqNorm (M * smulKron 1 (Weyl.synOf w (โ‡‘L) y) - smulKron 1 (Weyl.synOf w (โ‡‘L) y) * M) = (โ†‘(Fintype.card โ†ฅ(CL.perp L.ker)))โปยน * โˆ‘ v : โ†ฅ(CL.perp L.ker), ฮจ.stateSqNorm (M * smulKron 1 (w โ†‘v) - smulKron 1 (w โ†‘v) * M)

    lem:W: the two commutator errors agree exactly, without a dimension factor.

    source
    theorem MIPRE.Introspection.linear_measurement_commutator_parseval_avg {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {๐’ž : Type u_3} {๐’œ : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] {X : Type u_6} {A : Type u_7} [Fintype X] [Fintype A] (D : X โ†’ โ„) (w : (Fin n โ†’ F) โ†’ Matrix (Fin n โ†’ F) (Fin n โ†’ F) โ„‚) (L : X โ†’ (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) (ฮจ : BipartiteModel ๐’ž (Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) โ„ฌ) (M : X โ†’ A โ†’ Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) :
    โˆ‘ x : X, D x * โˆ‘ a : A, โˆ‘ y : Fin n โ†’ F, ฮจ.stateSqNorm (M x a * smulKron 1 (Weyl.synOf w (โ‡‘(L x)) y) - smulKron 1 (Weyl.synOf w (โ‡‘(L x)) y) * M x a) = โˆ‘ x : X, D x * ((โ†‘(Fintype.card โ†ฅ(CL.perp (L x).ker)))โปยน * โˆ‘ v : โ†ฅ(CL.perp (L x).ker), โˆ‘ a : A, ฮจ.stateSqNorm (M x a * smulKron 1 (w โ†‘v) - smulKron 1 (w โ†‘v) * M x a))

    The same identity summed over outcomes and averaged over questions.