Documentation

MIPRE.Foundations.Introspection.PauliTwirlDistance

Approximate Pauli mixing with explicit constants #

In the register model (Phase 4 of planning/mipco-track.md): the EPR state on the sampled register adjoined to an ancillary model ฮž (ฮž.reg (Fin n โ†’ F)), with register Paulis smulKron 1 (wZ v) and smulKron 1 (wX v); the Parseval transfers hold on any model whose first player's algebra carries the register.

source
theorem MIPRE.Introspection.star_smulKron_one_wZ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {๐’œ : Type u_4} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [StarModule โ„‚ ๐’œ] (v : Fin n โ†’ F) :
star (smulKron 1 (Weyl.wZ v)) = smulKron 1 (Weyl.wZ v)
source
theorem MIPRE.Introspection.star_smulKron_one_wX {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {R : Type u_6} [Ring R] [StarRing R] [Algebra โ„‚ R] [StarModule โ„‚ R] (v : Fin n โ†’ F) :
star (smulKron 1 (Weyl.wX v)) = smulKron 1 (Weyl.wX v)
source
theorem MIPRE.Introspection.dephaseZ_eq_unitaryTwirl {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {๐’œ : Type u_4} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [StarModule โ„‚ ๐’œ] (M : Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) :
dephaseZ M = unitaryTwirl (fun (x : Fin n โ†’ F) => (โ†‘(Fintype.card (Fin n โ†’ F)))โปยน) (fun (v : Fin n โ†’ F) => smulKron 1 (Weyl.wZ v)) M

The concrete Z dephasing is the uniform unitary twirl.

source
theorem MIPRE.Introspection.averageX_eq_unitaryTwirl {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {๐’œ : Type u_4} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [StarModule โ„‚ ๐’œ] (S : Submodule F (Fin n โ†’ F)) (M : Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ) :
averageX S M = unitaryTwirl (fun (x : โ†ฅS) => (โ†‘(Fintype.card โ†ฅS))โปยน) (fun (v : โ†ฅS) => smulKron 1 (Weyl.wX โ†‘v)) M

The concrete kernel averaging is the uniform X twirl.

source
theorem MIPRE.Introspection.smulKron_one_mul_self {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {R : Type u_6} [Ring R] [Algebra โ„‚ R] {P : Matrix (Fin n โ†’ F) (Fin n โ†’ F) โ„‚} (hP : P * P = 1) :
smulKron 1 P * smulKron 1 P = 1
source
theorem MIPRE.Introspection.pauli_twirl_dist_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {A : Type u_2} [Fintype A] {๐’ž : Type u_3} {๐’œ : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [StarModule โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [StarProper ๐’œ] (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (M : POVMIn A (Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ)) :
โˆ‘ a : A, (ฮž.reg (Fin n โ†’ F)).stateSqNorm (averageX L.ker (dephaseZ (M.op a)) - M.op a) โ‰ค 4 * ((โ†‘(Fintype.card (Fin n โ†’ F)))โปยน * โˆ‘ v : Fin n โ†’ F, โˆ‘ a : A, (ฮž.reg (Fin n โ†’ F)).stateSqNorm (M.op a * smulKron 1 (Weyl.wZ v) - smulKron 1 (Weyl.wZ v) * M.op a)) + 4 * ((โ†‘(Fintype.card โ†ฅL.ker))โปยน * โˆ‘ v : โ†ฅL.ker, โˆ‘ a : A, (ฮž.reg (Fin n โ†’ F)).stateSqNorm (M.op a * smulKron 1 (Weyl.wX โ†‘v) - smulKron 1 (Weyl.wX โ†‘v) * M.op a))

Twirling by all Z operators and kernel X operators costs four times each commutator error.

source
theorem MIPRE.Introspection.fine_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 โ„‚ โ„ฌ] (ฮจ : 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 Weyl.wZ (โ‡‘LinearMap.id) y) - smulKron 1 (Weyl.synOf Weyl.wZ (โ‡‘LinearMap.id) y) * M) = (โ†‘(Fintype.card (Fin n โ†’ F)))โปยน * โˆ‘ v : Fin n โ†’ F, ฮจ.stateSqNorm (M * smulKron 1 (Weyl.wZ v) - smulKron 1 (Weyl.wZ v) * M)

Fine Z readouts transfer to the uniform full-register Pauli error.

source
theorem MIPRE.Introspection.kernel_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 โ„‚ โ„ฌ] (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 Weyl.wX (โ‡‘(CL.lperp L)) y) - smulKron 1 (Weyl.synOf Weyl.wX (โ‡‘(CL.lperp L)) y) * M) = (โ†‘(Fintype.card โ†ฅL.ker))โปยน * โˆ‘ v : โ†ฅL.ker, ฮจ.stateSqNorm (M * smulKron 1 (Weyl.wX โ†‘v) - smulKron 1 (Weyl.wX โ†‘v) * M)

The L-perpendicular readout transfers to the uniform Pauli error on ker L.

source
theorem MIPRE.Introspection.pauli_twirl_readout_dist_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : โ„•} {A : Type u_2} [Fintype A] {๐’ž : Type u_3} {๐’œ : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [StarModule โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [StarProper ๐’œ] (L : (Fin n โ†’ F) โ†’โ‚—[F] Fin n โ†’ F) (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (M : POVMIn A (Matrix (Fin n โ†’ F) (Fin n โ†’ F) ๐’œ)) :
โˆ‘ a : A, (ฮž.reg (Fin n โ†’ F)).stateSqNorm (averageX L.ker (dephaseZ (M.op a)) - M.op a) โ‰ค 4 * โˆ‘ a : A, โˆ‘ y : Fin n โ†’ F, (ฮž.reg (Fin n โ†’ F)).stateSqNorm (M.op a * smulKron 1 (Weyl.synOf Weyl.wZ (โ‡‘LinearMap.id) y) - smulKron 1 (Weyl.synOf Weyl.wZ (โ‡‘LinearMap.id) y) * M.op a) + 4 * โˆ‘ a : A, โˆ‘ y : Fin n โ†’ F, (ฮž.reg (Fin n โ†’ F)).stateSqNorm (M.op a * smulKron 1 (Weyl.synOf Weyl.wX (โ‡‘(CL.lperp L)) y) - smulKron 1 (Weyl.synOf Weyl.wX (โ‡‘(CL.lperp L)) y) * M.op a)

The twirl error controlled directly by the two projective-readout commutator errors.