Entry formulas for Pauli twirls with an ancillary space

Stated for block matrices over an arbitrary algebra 𝒜 (Phase 4 of planning/mipco-track.md): the register is Fin n → F, the ancilla is abstract, an operator of register and ancilla is a matrix Matrix (Fin n → F) (Fin n → F) 𝒜, and a register operator A is smulKron 1 A. The matrix statements, on (Fin n → F) × H, are the case 𝒜 = Matrix H H ℂ.

theorem MIPRE.Introspection.smulKron_wZ_mul_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (v x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : (smulKron 1 (Weyl.wZ v) * M) x y = sgn (Weyl.trDot v x) • M x y

theorem MIPRE.Introspection.mul_smulKron_wZ_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (v x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : (M * smulKron 1 (Weyl.wZ v)) x y = sgn (Weyl.trDot v y) • M x y

theorem MIPRE.Introspection.smulKron_wZ_conjugate_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (v x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : (smulKron 1 (Weyl.wZ v) * M * smulKron 1 (Weyl.wZ v)) x y = sgn (Weyl.trDot v (x + y)) • M x y

noncomputable def MIPRE.Introspection.dephaseZ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : Matrix (Fin n → F) (Fin n → F) 𝒜

Average over the full Z Pauli family on the register.

Equations

• MIPRE.Introspection.dephaseZ M = (↑(Fintype.card (Fin n → F)))⁻¹ • ∑ v : Fin n → F, MIPRE.smulKron 1 (MIPRE.Weyl.wZ v) * M * MIPRE.smulKron 1 (MIPRE.Weyl.wZ v)

theorem MIPRE.Introspection.dephaseZ_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : dephaseZ M x y = if x = y then M x y else 0

The full Z twirl removes precisely the off-diagonal blocks in the sampled register.

theorem MIPRE.Introspection.smulKron_wX_mul_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (v x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : (smulKron 1 (Weyl.wX v) * M) x y = M (x + v) y

theorem MIPRE.Introspection.mul_smulKron_wX_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (v x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : (M * smulKron 1 (Weyl.wX v)) x y = M x (y + v)

theorem MIPRE.Introspection.smulKron_wX_conjugate_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (v x y : Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : (smulKron 1 (Weyl.wX v) * M * smulKron 1 (Weyl.wX v)) x y = M (x + v) (y + v)

noncomputable def MIPRE.Introspection.averageX {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (K : Submodule F (Fin n → F)) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : Matrix (Fin n → F) (Fin n → F) 𝒜

Average the X Pauli conjugations belonging to a subspace.

Equations

• MIPRE.Introspection.averageX K M = (↑(Fintype.card ↥K))⁻¹ • ∑ v : ↥K, MIPRE.smulKron 1 (MIPRE.Weyl.wX ↑v) * M * MIPRE.smulKron 1 (MIPRE.Weyl.wX ↑v)

noncomputable def MIPRE.Introspection.averagedBlock {F : Type u_1} [Field F] [Fintype F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (K : Submodule F (Fin n → F)) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) (x : Fin n → F) : 𝒜

The diagonal ancillary block obtained by averaging the fiber through x.

Equations

• MIPRE.Introspection.averagedBlock K M x = (↑(Fintype.card ↥K))⁻¹ • ∑ v : ↥K, M (x + ↑v) (x + ↑v)

theorem MIPRE.Introspection.averageX_dephaseZ_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (K : Submodule F (Fin n → F)) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) (x y : Fin n → F) : averageX K (dephaseZ M) x y = if x = y then averagedBlock K M x else 0

First dephasing, then averaging X(K), leaves only the averaged diagonal blocks.

theorem MIPRE.Introspection.averagedBlock_eq_of_sub_mem {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (K : Submodule F (Fin n → F)) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) (x y : Fin n → F) (hxy : x - y ∈ K) : averagedBlock K M x = averagedBlock K M y

The averaged ancillary block is constant on each coset of the twirled subspace.

theorem MIPRE.Introspection.synOf_wZ_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (L : (Fin n → F) →ₗ[F] Fin n → F) (a x y : Fin n → F) : Weyl.synOf Weyl.wZ (⇑L) a x y = if x = y then if L x = a then 1 else 0 else 0

theorem MIPRE.Introspection.linear_twirl_blocks {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [Algebra ℂ 𝒜] (L : (Fin n → F) →ₗ[F] Fin n → F) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) : averageX L.ker (dephaseZ M) = ∑ a : Fin n → F, smulKron (averagedBlock L.ker M (linearPreimage L a)) (Weyl.synOf Weyl.wZ (⇑L) a)

The exact block decomposition used by the hiding argument, including an arbitrary ancilla.