Exact Pauli twirling on a field-linear subspace

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

Equations

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

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

Equations

• MIPRE.Introspection.twirlZ K M = (↑(Fintype.card ↥K))⁻¹ • ∑ v : ↥K, MIPRE.Weyl.wZ ↑v * M * MIPRE.Weyl.wZ ↑v

theorem MIPRE.Introspection.conjugate_wZ_by_wX {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (v u : Fin n → F) : Weyl.wX v * Weyl.wZ u * Weyl.wX v = sgn (Weyl.trDot v u) • Weyl.wZ u

theorem MIPRE.Introspection.conjugate_wX_by_wZ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (v u : Fin n → F) : Weyl.wZ v * Weyl.wX u * Weyl.wZ v = sgn (Weyl.trDot v u) • Weyl.wX u

theorem MIPRE.Introspection.twirlX_wZ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (K : Submodule F (Fin n → F)) (u : Fin n → F) : twirlX K (Weyl.wZ u) = if u ∈ CL.perp K then Weyl.wZ u else 0

The X(K) twirl retains exactly those Z operators in the dot-product annihilator.

theorem MIPRE.Introspection.twirlZ_wX {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (K : Submodule F (Fin n → F)) (u : Fin n → F) : twirlZ K (Weyl.wX u) = if u ∈ CL.perp K then Weyl.wX u else 0

The dual Z(K) twirl has the same annihilator criterion.