Notation: Pauli Operators

Statement

For qubits labeled by vertices v of a graph or indices i, we denote by X_v (or X_i) the Pauli-X operator acting on qubit v (or i), and similarly Z_v (or Z_i) for Pauli-Z. A product of Pauli operators is written as ∏_{v ∈ S} X_v for a set S of qubit labels. The identity operator is denoted 𝟙. For a Pauli operator P, we denote by S_X(P) the X-type support (sites where P acts via X or Y) and S_Z(P) the Z-type support (sites where P acts via Y or Z).

Main Results

• PauliOp: multi-qubit Pauli operator as a pair of binary vectors (x, z) ∈ (ZMod 2)^V × (ZMod 2)^V
• PauliOp.pauliX, PauliOp.pauliZ: single-site Pauli-X and Pauli-Z operators
• PauliOp.prodX, PauliOp.prodZ: products of Pauli operators over a finset
• PauliOp.supportX, PauliOp.supportZ: X-type and Z-type supports
• PauliOp.mul: multiplication of Pauli operators (pointwise XOR of binary vectors)

Corollaries

• Support characterization lemmas
• Product support lemmas
• Identity and single-site support computations

Definition of Pauli operators

structure PauliOp (V : Type u_2) : Type u_2

Pauli operators on qubits labeled by type V, represented as pairs of binary vectors (xVec, zVec) ∈ (ZMod 2)^V × (ZMod 2)^V. The pair (x, z) represents the Pauli operator ⊗_v X_v^{x_v} Z_v^{z_v}.

• (0, 0) at site v means identity I
• (1, 0) at site v means X
• (0, 1) at site v means Z
• (1, 1) at site v means Y (up to phase)

• xVec : V → ZMod 2
• zVec : V → ZMod 2

theorem PauliOp.ext {V : Type u_2} {x y : PauliOp V} (xVec : x.xVec = y.xVec) (zVec : x.zVec = y.zVec) : x = y

theorem PauliOp.ext_iff {V : Type u_2} {x y : PauliOp V} : x = y ↔ x.xVec = y.xVec ∧ x.zVec = y.zVec

Identity operator

def PauliOp.id (V : Type u_2) : PauliOp V

The identity Pauli operator (acts as identity on all qubits).

Equations

• PauliOp.id V = { xVec := 0, zVec := 0 }

Single-site Pauli operators

def PauliOp.pauliX {V : Type u_1} [DecidableEq V] (v : V) : PauliOp V

Pauli-X operator acting on qubit v.

Equations

• PauliOp.pauliX v = { xVec := Pi.single v 1, zVec := 0 }

def PauliOp.pauliZ {V : Type u_1} [DecidableEq V] (v : V) : PauliOp V

Pauli-Z operator acting on qubit v.

Equations

• PauliOp.pauliZ v = { xVec := 0, zVec := Pi.single v 1 }

def PauliOp.pauliY {V : Type u_1} [DecidableEq V] (v : V) : PauliOp V

Pauli-Y operator acting on qubit v (= X_v Z_v up to phase).

Equations

• PauliOp.pauliY v = { xVec := Pi.single v 1, zVec := Pi.single v 1 }

Multiplication (pointwise XOR of binary vectors)

def PauliOp.mul {V : Type u_1} (P Q : PauliOp V) : PauliOp V

Product of two Pauli operators (pointwise addition of binary vectors in ZMod 2). This captures the Pauli group multiplication up to phase.

Equations

• P.mul Q = { xVec := P.xVec + Q.xVec, zVec := P.zVec + Q.zVec }

instance PauliOp.instMul {V : Type u_1} : Mul (PauliOp V)

Equations

• PauliOp.instMul = { mul := PauliOp.mul }

instance PauliOp.instOne {V : Type u_1} : One (PauliOp V)

Equations

• PauliOp.instOne = { one := { xVec := 0, zVec := 0 } }

@[simp]

theorem PauliOp.one_xVec {V : Type u_1} : xVec 1 = 0

@[simp]

theorem PauliOp.one_zVec {V : Type u_1} : zVec 1 = 0

@[simp]

theorem PauliOp.mul_xVec {V : Type u_1} (P Q : PauliOp V) : (P * Q).xVec = P.xVec + Q.xVec

@[simp]

theorem PauliOp.mul_zVec {V : Type u_1} (P Q : PauliOp V) : (P * Q).zVec = P.zVec + Q.zVec

theorem PauliOp.mul_comm {V : Type u_1} (P Q : PauliOp V) : P * Q = Q * P

theorem PauliOp.mul_assoc {V : Type u_1} (P Q R : PauliOp V) : P * Q * R = P * (Q * R)

theorem PauliOp.one_mul {V : Type u_1} (P : PauliOp V) : 1 * P = P

theorem PauliOp.mul_one {V : Type u_1} (P : PauliOp V) : P * 1 = P

theorem PauliOp.mul_self {V : Type u_1} (P : PauliOp V) : P * P = 1

instance PauliOp.instCommGroup {V : Type u_1} : CommGroup (PauliOp V)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PauliOp.inv_eq_self {V : Type u_1} (P : PauliOp V) : P⁻¹ = P

Products of Pauli operators over finite sets

def PauliOp.prodX {V : Type u_1} [DecidableEq V] (S : Finset V) : PauliOp V

Product of Pauli-X operators over a finset S of qubit labels: ∏_{v ∈ S} X_v

Equations

• PauliOp.prodX S = { xVec := fun (v : V) => if v ∈ S then 1 else 0, zVec := 0 }

def PauliOp.prodZ {V : Type u_1} [DecidableEq V] (S : Finset V) : PauliOp V

Product of Pauli-Z operators over a finset S of qubit labels: ∏_{v ∈ S} Z_v

Equations

• PauliOp.prodZ S = { xVec := 0, zVec := fun (v : V) => if v ∈ S then 1 else 0 }

@[simp]

theorem PauliOp.prodX_empty {V : Type u_1} [DecidableEq V] : prodX ∅ = 1

@[simp]

theorem PauliOp.prodZ_empty {V : Type u_1} [DecidableEq V] : prodZ ∅ = 1

X-type and Z-type support

def PauliOp.supportX {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) : Finset V

X-type support: the set of sites where P acts via X or Y (i.e., where xVec is nonzero).

Equations

• P.supportX = {v : V | P.xVec v ≠ 0}

def PauliOp.supportZ {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) : Finset V

Z-type support: the set of sites where P acts via Y or Z (i.e., where zVec is nonzero).

Equations

• P.supportZ = {v : V | P.zVec v ≠ 0}

def PauliOp.support {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) : Finset V

Full support: sites where P acts non-trivially (via X, Y, or Z).

Equations

• P.support = {v : V | P.xVec v ≠ 0 ∨ P.zVec v ≠ 0}

def PauliOp.weight {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) : ℕ

Weight of a Pauli operator: number of qubits on which it acts non-trivially.

Equations

• P.weight = P.support.card

Support membership characterizations

@[simp]

theorem PauliOp.mem_supportX {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) (v : V) : v ∈ P.supportX ↔ P.xVec v ≠ 0

@[simp]

theorem PauliOp.mem_supportZ {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) (v : V) : v ∈ P.supportZ ↔ P.zVec v ≠ 0

@[simp]

theorem PauliOp.mem_support {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) (v : V) : v ∈ P.support ↔ P.xVec v ≠ 0 ∨ P.zVec v ≠ 0

In ZMod 2, nonzero means equal to 1

@[simp]

theorem PauliOp.mem_supportX_iff {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) (v : V) : v ∈ P.supportX ↔ P.xVec v = 1

@[simp]

theorem PauliOp.mem_supportZ_iff {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) (v : V) : v ∈ P.supportZ ↔ P.zVec v = 1

Identity support

@[simp]

theorem PauliOp.supportX_one {V : Type u_1} [DecidableEq V] [Fintype V] : supportX 1 = ∅

@[simp]

theorem PauliOp.supportZ_one {V : Type u_1} [DecidableEq V] [Fintype V] : supportZ 1 = ∅

@[simp]

theorem PauliOp.support_one {V : Type u_1} [DecidableEq V] [Fintype V] : support 1 = ∅

@[simp]

theorem PauliOp.weight_one {V : Type u_1} [DecidableEq V] [Fintype V] : weight 1 = 0

Single-site operator supports

@[simp]

theorem PauliOp.supportX_pauliX {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : (pauliX v).supportX = {v}

@[simp]

theorem PauliOp.supportZ_pauliX {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : (pauliX v).supportZ = ∅

@[simp]

theorem PauliOp.supportX_pauliZ {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : (pauliZ v).supportX = ∅

@[simp]

theorem PauliOp.supportZ_pauliZ {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : (pauliZ v).supportZ = {v}

@[simp]

theorem PauliOp.supportX_pauliY {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : (pauliY v).supportX = {v}

@[simp]

theorem PauliOp.supportZ_pauliY {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : (pauliY v).supportZ = {v}

Product support characterizations

theorem PauliOp.supportX_prodX {V : Type u_1} [DecidableEq V] [Fintype V] (S : Finset V) : (prodX S).supportX = S

theorem PauliOp.supportZ_prodX {V : Type u_1} [DecidableEq V] [Fintype V] (S : Finset V) : (prodX S).supportZ = ∅

theorem PauliOp.supportX_prodZ {V : Type u_1} [DecidableEq V] [Fintype V] (S : Finset V) : (prodZ S).supportX = ∅

theorem PauliOp.supportZ_prodZ {V : Type u_1} [DecidableEq V] [Fintype V] (S : Finset V) : (prodZ S).supportZ = S

Support union bound

theorem PauliOp.support_eq_supportX_union_supportZ {V : Type u_1} [DecidableEq V] [Fintype V] (P : PauliOp V) : P.support = P.supportX ∪ P.supportZ

Pauli-X single-site and product relationship

theorem PauliOp.pauliX_eq_prodX_singleton {V : Type u_1} [DecidableEq V] (v : V) : pauliX v = prodX {v}

theorem PauliOp.pauliZ_eq_prodZ_singleton {V : Type u_1} [DecidableEq V] (v : V) : pauliZ v = prodZ {v}