Clifford project

4. Pauli matrices🔗

This section defines the generalized Pauli X and Z matrices on ℂ^d and proves some basic fats about them. Throughout this section we assume that d ≥ 1.

Lean codevariable (d : ℕ) [NeZero d]

The generalized Pauli X matrix corresponds to adding one modulo d.

Definition4.29
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Lemma 4.30
Loading preview
Hover a group entry to preview it.
✓L∃∀N
Used by 2
Hover a use site to preview it.
Preview
Definition 5.46
Loading preview
Hover a use site to preview it.
OwnerMaris Ozols

The d-dimensional Pauli X matrix acts as follows: X \ket{k} = \ket{k+1} where k ∈ ℤ_d and addition is modulo d.

Lean code for Definition4.29def X : Matrix (ZMod d) (ZMod d) ℂ := Matrix.of fun i j => if j + 1 = i then 1 else 0

Powers of the Pauli X matrix.

Lemma4.30
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 0
OwnerCarli Bruinsma

The n-th power of the d-dimensional Pauli X matrix acts on basis vectors as X^n \ket{k} = \ket{k + n \mod d}.

Lean code for Lemma4.30lemma X_pow_pos_n (n : ℕ) : X d ^ n = Matrix.of (fun i j => if j + (n : ZMod d) = i then 1 else 0) := d:ℕinst✝:NeZero dn:ℕ⊢ X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0 induction n with d:ℕinst✝:NeZero d⊢ X d ^ 0 = Matrix.of fun i j => if j + ↑0 = i then 1 else 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (X d ^ 0) i j = Matrix.of (fun i j => if j + ↑0 = i then 1 else 0) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod dhij:i = j ↔ j = i⊢ (X d ^ 0) i j = Matrix.of (fun i j => if j + ↑0 = i then 1 else 0) i j All goals completed! 🐙 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0⊢ X d ^ (n + 1) = Matrix.of fun i j => if j + ↑(n + 1) = i then 1 else 0 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod d⊢ (X d ^ (n + 1)) i j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i j d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod d⊢ ∑ j_1, Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i j_1 * X d j_1 j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i j have hfun : ∀ (x : ZMod d), x ≠ (j + (1 : ZMod d)) → X d x j = 0 := d:ℕinst✝:NeZero dn:ℕ⊢ X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod d⊢ ∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + 1 = i then 1 else 0) x j = 0 intro x d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dx:ZMod dh:x ≠ j + 1⊢ Matrix.of (fun i j => if j + 1 = i then 1 else 0) x j = 0 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dx:ZMod dh:x ≠ j + 1⊢ ¬j + 1 = x d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dx:ZMod dh:x ≠ j + 1h':j + 1 = x⊢ False d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dx:ZMod dh:x ≠ j + 1h':x = j + 1⊢ False All goals completed! 🐙 have hfun' : ∀ (x : ZMod d), x ≠ (j + (1 : ZMod d)) → Matrix.of (fun i j => if j + (n : ZMod d) = i then 1 else 0) i x * X d x j = 0 := d:ℕinst✝:NeZero dn:ℕ⊢ X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0 intro x d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0x:ZMod dh:x ≠ j + 1⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dx:ZMod dh:x ≠ j + 1hfun:X d x j = 0⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0 All goals completed! 🐙 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i (j + 1) * X d (j + 1) j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i j d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:j + (↑n + 1) = i⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i (j + 1) * X d (j + 1) j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i jd:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = i⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i (j + 1) * X d (j + 1) j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i j d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:j + (↑n + 1) = i⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i (j + 1) * X d (j + 1) j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i jd:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = i⊢ Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i (j + 1) * X d (j + 1) j = Matrix.of (fun i j => if j + ↑(n + 1) = i then 1 else 0) i j d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = i⊢ j + 1 + ↑n = i → X d (j + 1) j = 0; d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:j + 1 + ↑n = i⊢ (if j + 1 + ↑n = i then X d (j + 1) j else 0) = 1d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = i⊢ j + 1 + ↑n = i → X d (j + 1) j = 0; d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = i⊢ j + 1 + ↑n = i → X d (j + 1) j = 0 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = ihj:j + 1 + ↑n = i⊢ X d (j + 1) j = 0 d:ℕinst✝:NeZero dn:ℕhind:X d ^ n = Matrix.of fun i j => if j + ↑n = i then 1 else 0i:ZMod dj:ZMod dhfun:∀ (x : ZMod d), x ≠ j + 1 → X d x j = 0hfun':∀ (x : ZMod d), x ≠ j + 1 → Matrix.of (fun i j => if j + ↑n = i then 1 else 0) i x * X d x j = 0h:¬j + (↑n + 1) = ihj:j + (↑n + 1) = i⊢ X d (j + 1) j = 0 All goals completed! 🐙

The Pauli X matrix has order d.

Lemma4.31
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 0
OwnerGina Muuss

The d-th power of the d-dimensional Pauli X matrix is the identity matrix: X^d = I.

Lean code for Lemma4.31lemma X_pow_d_eq_one : X d ^ d = 1 := d:ℕinst✝:NeZero d⊢ X d ^ d = 1 d:ℕinst✝:NeZero d⊢ (Matrix.of fun i j => if j + ↑d = i then 1 else 0) = 1 d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ Matrix.of (fun i j => if j + ↑d = i then 1 else 0) i j = 1 i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (if j = i then 1 else 0) = 1 i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (if i = j then 1 else 0) = 1 i j All goals completed! 🐙

The generalized Pauli Z matrix is diagonal and introduces a phase ω to each standard basis vector \ket{k}.

Definition4.32
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀N
Used by 2
Hover a use site to preview it.
Preview
Definition 5.46
Loading preview
Hover a use site to preview it.
OwnerMaris Ozols

The d-dimensional Pauli Z matrix acts as follows: Z \ket{k} = ω^k \ket{k} where k ∈ ℤ_d and ω is the primitive d-th root of unity from Definition 2.3.

Lean code for Definition4.32noncomputable def Z : Matrix (ZMod d) (ZMod d) ℂ := Matrix.of fun i j => if i = j then ω d ^ i.val else 0

The Pauli Z matrix also has order d.

Lemma4.33
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 0
OwnerCarli Bruinsma

The d-th power of the d-dimensional Pauli Z matrix is the identity matrix: Z^d = I.

Lean codelemma Z_pow_n (n : ℕ) : Z d ^ n = Matrix.diagonal (fun i => ω d ^ (i.val * n)):= d:ℕinst✝:NeZero dn:ℕ⊢ Z d ^ n = Matrix.diagonal fun i => ω d ^ (i.val * n) d:ℕinst✝:NeZero dn:ℕhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.val⊢ Z d ^ n = Matrix.diagonal fun i => ω d ^ (i.val * n) d:ℕinst✝:NeZero dn:ℕhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.val⊢ Matrix.diagonal ((fun i => ω d ^ i.val) ^ n) = Matrix.diagonal fun i => ω d ^ (i.val * n) d:ℕinst✝:NeZero dn:ℕhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.val⊢ ∀ (i : ZMod d), (ω d ^ i.val) ^ n = ω d ^ (i.val * n) d:ℕinst✝:NeZero dn:ℕhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.vali:ZMod d⊢ (ω d ^ i.val) ^ n = ω d ^ (i.val * n) All goals completed! 🐙
Lean code for Lemma4.33lemma Z_pow_d_eq_one : (Z d) ^ d = 1 := d:ℕinst✝:NeZero d⊢ Z d ^ d = 1 d:ℕinst✝:NeZero d⊢ (Matrix.diagonal fun i => ω d ^ (i.val * d)) = 1 d:ℕinst✝:NeZero d⊢ (fun i => ω d ^ (i.val * d)) = 1 d:ℕinst✝:NeZero di:ZMod d⊢ ω d ^ (i.val * d) = 1 i d:ℕinst✝:NeZero di:ZMod d⊢ 1 = 1 i All goals completed! 🐙

Pauli X and Z commute up to a phase.

Lemma4.35
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 0
OwnerGina Muuss

Pauli X and Z matrices satisfy the following commutation relation: Z X = ω X Z.

Lean code for Lemma4.35lemma ZX_eq_omega_mul_XZ : Z d * X d = ω d • (X d * Z d) := d:ℕinst✝:NeZero d⊢ Z d * X d = ω d • (X d * Z d) d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (Z d * X d) i j = (ω d • (X d * Z d)) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ ∑ j_1, Z d i j_1 * X d j_1 j = ω d • ∑ j_1, X d i j_1 * Z d j_1 j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ ∑ j_1, Matrix.of (fun i j => if i = j then ω d ^ i.val else 0) i j_1 * Matrix.of (fun i j => if j + 1 = i then 1 else 0) j_1 j = ω d • ∑ j_1, Matrix.of (fun i j => if j + 1 = i then 1 else 0) i j_1 * Matrix.of (fun i j => if i = j then ω d ^ i.val else 0) j_1 j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (if i = j + 1 then ω d ^ i.val else 0) = if j + 1 = i then ω d * ω d ^ j.val else 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (if i = j + 1 then ω d ^ i.val else 0) = if i = j + 1 then ω d * ω d ^ j.val else 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dh:i = j + 1⊢ (if i = j + 1 then ω d ^ i.val else 0) = if i = j + 1 then ω d * ω d ^ j.val else 0d:ℕinst✝:NeZero di:ZMod dj:ZMod dh:¬i = j + 1⊢ (if i = j + 1 then ω d ^ i.val else 0) = if i = j + 1 then ω d * ω d ^ j.val else 0 /- Case 1: h : i = j + 1-/ d:ℕinst✝:NeZero di:ZMod dj:ZMod dh:i = j + 1⊢ (if i = j + 1 then ω d ^ i.val else 0) = if i = j + 1 then ω d * ω d ^ j.val else 0 All goals completed! 🐙 /- Case 2: h : i ≠ j + 1-/ All goals completed! 🐙

And so do their powers.

Lemma4.36
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
⚠L∃∀Nused by 0
OwnerDaan Planken

Pauli X and Z matrices satisfy the following commutation relation: Z^k X^ℓ = ω^{k·ℓ} X^ℓ Z^k.

Lean code for Lemma4.36lemma declaration uses `sorry`Z_pow_X_pow_eq_omega_mul_X_pow_Z_pow (k : ℕ) (ℓ : ℕ) : (Z d) ^ k * (X d) ^ ℓ = (ω d) ^ (k * ℓ) • ((X d) ^ ℓ * (Z d) ^ k) := d:ℕinst✝:NeZero dk:ℕℓ:ℕ⊢ Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k) induction ℓ with d:ℕinst✝:NeZero dk:ℕ⊢ Z d ^ k * X d ^ 0 = ω d ^ (k * 0) • (X d ^ 0 * Z d ^ k) All goals completed! 🐙 d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)⊢ Z d ^ k * X d ^ (ℓ + 1) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) nth_rw 1 [pow_succ'd:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)⊢ Z d ^ k * (X d * X d ^ ℓ) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) nth_rw 1 [← mul_assocd:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)⊢ Z d ^ k * X d * X d ^ ℓ = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) have h : Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ := d:ℕinst✝:NeZero dk:ℕℓ:ℕ⊢ Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k) All goals completed! 🐙 d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ k • X d * Z d ^ k * X d ^ ℓ = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) nth_rw 1 [mul_assocd:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ k • X d * (Z d ^ k * X d ^ ℓ) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) --nth_rw 1 [mul_comm] d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ k • (X d * (Z d ^ k * X d ^ ℓ)) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ X d * ω d ^ k • (Z d ^ k * X d ^ ℓ) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ X d * ω d ^ k • ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ X d * (ω d ^ k * ω d ^ (k * ℓ)) • (X d ^ ℓ * Z d ^ k) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ (ω d ^ k * ω d ^ (k * ℓ)) • (X d * (X d ^ ℓ * Z d ^ k)) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ (k + k * ℓ) • (X d * (X d ^ ℓ * Z d ^ k)) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ (k * (1 + ℓ)) • (X d * (X d ^ ℓ * Z d ^ k)) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ (k * (1 + ℓ)) • (X d * X d ^ ℓ * Z d ^ k) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) d:ℕinst✝:NeZero dk:ℕℓ:ℕih:Z d ^ k * X d ^ ℓ = ω d ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k)h:Z d ^ k * X d * X d ^ ℓ = ω d ^ k • X d * Z d ^ k * X d ^ ℓ⊢ ω d ^ (k * (1 + ℓ)) • (X d ^ (ℓ + 1) * Z d ^ k) = ω d ^ (k * (ℓ + 1)) • (X d ^ (ℓ + 1) * Z d ^ k) All goals completed! 🐙 --#check Matrix.mul_smul /-rw [smul_mul_assoc] rw [ih] rw [smul_smul] rw [← pow_add] rw [add_comm] rw [← mul_add_one] induction k with | zero => simp rw [pow_succ'] | succ k ih2 =>-/

And also backwards

Lean codelemma X_pow_Z_pow_eq_omega_mul_Z_pow_X_pow (k : ZMod d) (l : ZMod d) : (X d) ^ k.val * (Z d) ^ l.val = (ω d) ^ (-(k * l)).val • ((Z d) ^ l.val * (X d) ^ k.val) := d:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ (-(k * l)).val • (Z d ^ l.val * X d ^ k.val) d:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ (-(k * l)).val • ω d ^ (l.val * k.val) • (X d ^ k.val * Z d ^ l.val) d:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = (ω d ^ (-(k * l)).val * ω d ^ (l.val * k.val)) • (X d ^ k.val * Z d ^ l.val) nth_rw 2 [omega_pow_n_mod_dd:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = (ω d ^ (-(k * l)).val * ω d ^ (l.val * k.val % d)) • (X d ^ k.val * Z d ^ l.val) d:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ ((-(k * l)).val + (l * k).val) • (X d ^ k.val * Z d ^ l.val) d:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ (-(k * l) + l * k).val • (X d ^ k.val * Z d ^ l.val) d:ℕinst✝:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ 0 • (X d ^ k.val * Z d ^ l.val) All goals completed! 🐙
Lemma4.38
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 0
OwnerCarli Bruinsma

Powers of Pauli X and Z satisfy X^n = X^{n \% d} Z^n = Z^{n \% d}

Lean code for Lemma4.38theorem X_pow_n_mod_d (n : ℕ): X d ^ n = X d ^ (n % ↑d) := pow_eq_pow_mod n (X_pow_d_eq_one d) theorem Z_pow_n_mod_d (n : ℕ): Z d ^ n = Z d ^ (n % ↑d) := pow_eq_pow_mod n (Z_pow_d_eq_one d)
Lemma4.39
Group: Core properties of the single-qudit Pauli matrices. (8)
Hover another entry in this group to preview it.
Preview
Definition 4.29
Loading preview
Hover a group entry to preview it.
✓L∃∀Nused by 0
OwnerGina Muuss

X^{†} = X^(-1).

Lean code for Lemma4.39lemma X_inv : (X d).conjTranspose = (X d)^((-1 : ZMod d).val) := d:ℕinst✝:NeZero d⊢ (X d).conjTranspose = X d ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (X d).conjTranspose i j = (X d ^ (-1).val) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (X d).conjTranspose i j = Matrix.of (fun i j => if j + ↑(-1).val = i then 1 else 0) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ star (X d j i) = Matrix.of (fun i j => if j + ↑(-1).val = i then 1 else 0) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ star (Matrix.of (fun i j => if j + 1 = i then 1 else 0) j i) = Matrix.of (fun i j => if j + ↑(-1).val = i then 1 else 0) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (if i + 1 = j then 1 else 0) = if j + -1 = i then 1 else 0 have hfalso: (k: ZMod d) → k + 1 + ↑((-1 : ℤ) % d).toNat = k := d:ℕinst✝:NeZero d⊢ (X d).conjTranspose = X d ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dk:ZMod d⊢ k + 1 + ↑(-1 % ↑d).toNat = k have h3 : 0 ≤ ((-1 : ℤ) % d) := d:ℕinst✝:NeZero d⊢ (X d).conjTranspose = X d ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dk:ZMod d⊢ ↑d ≠ 0 All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dk:ZMod dh3:0 ≤ -1 % ↑d⊢ k + 1 + ↑(-1 % ↑d) = k All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:i + 1 = jh2:j + -1 = i⊢ 1 = 1d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:i + 1 = jh2:¬j + -1 = i⊢ 1 = 0d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:j + -1 = i⊢ 0 = 1d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:¬j + -1 = i⊢ 0 = 0; d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:i + 1 = jh2:¬j + -1 = i⊢ 1 = 0d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:j + -1 = i⊢ 0 = 1d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:¬j + -1 = i⊢ 0 = 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:i + 1 = jh2:¬j + -1 = i⊢ 1 = 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:i + 1 = jh2:¬j + -1 = i⊢ False d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:i + 1 = jh2:¬i + 1 + -1 = i⊢ False All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:j + -1 = i⊢ 0 = 1 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:j + -1 = i⊢ False d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬j + (-1 + 1) = jh2:j + -1 = i⊢ False nth_rw 2 [add_commd:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬j + (1 + -1) = jh2:j + -1 = i⊢ False at h1 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬j + 1 + -1 = jh2:j + -1 = i⊢ False All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhfalso:∀ (k : ZMod d), k + 1 + ↑(-1 % ↑d).toNat = kh1:¬i + 1 = jh2:¬j + -1 = i⊢ 0 = 0 All goals completed! 🐙
Lean codelemma X_pow_eq_mod_d : (x: ℕ) → (y: ℕ) → (x % d = y % d → X d ^ x = X d ^ y ) := d:ℕinst✝:NeZero d⊢ ∀ (x y : ℕ), x % d = y % d → X d ^ x = X d ^ y intro x d:ℕinst✝:NeZero dx:ℕy:ℕ⊢ x % d = y % d → X d ^ x = X d ^ y d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ x = X d ^ y d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ (d * (x / d) + x % d) = X d ^ y d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ (d * (x / d) + x % d) = X d ^ (d * (y / d) + y % d) d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ (X d ^ d) ^ (x / d) * X d ^ (x % d) = (X d ^ d) ^ (y / d) * X d ^ (y % d) d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ 1 ^ (x / d) * X d ^ (x % d) = 1 ^ (y / d) * X d ^ (y % d) d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ (x % d) = X d ^ (y % d) All goals completed! 🐙
Lean codelemma X_inv_pow : (x: ZMod d) → ((X d)^(x.val)).conjTranspose = (X d)^((-x).val):= d:ℕinst✝:NeZero d⊢ ∀ (x : ZMod d), (X d ^ x.val).conjTranspose = X d ^ (-x).val d:ℕinst✝:NeZero dx:ZMod d⊢ (X d ^ x.val).conjTranspose = X d ^ (-x).val d:ℕinst✝:NeZero dx:ZMod d⊢ X d ^ ((-1).val * x.val) = X d ^ (-x).val d:ℕinst✝:NeZero dx:ZMod d⊢ (-1).val * x.val % d = (-x).val % d d:ℕinst✝:NeZero dx:ZMod d⊢ (-x).val = (-x).val % d All goals completed! 🐙
Lean codelemma Z_inv : (Z d).conjTranspose = (Z d)^((-1 : ZMod d).val) := d:ℕinst✝:NeZero d⊢ (Z d).conjTranspose = Z d ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ (Z d).conjTranspose i j = (Z d ^ (-1).val) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod d⊢ star (Z d j i) = (Z d ^ (-1).val) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.val⊢ star (Z d j i) = (Z d ^ (-1).val) i j d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.val⊢ star (if j = i then ω d ^ j.val else 0) = if i = j then ((fun i => ω d ^ i.val) ^ (-1).val) i else 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.val⊢ (starRingEnd ℂ) (if j = i then ω d ^ j.val else 0) = if i = j then (ω d ^ i.val) ^ (-1).val else 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ (starRingEnd ℂ) (ω d ^ j.val) = (ω d ^ i.val) ^ (-1).vald:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:¬i = j⊢ (starRingEnd ℂ) (ω d ^ j.val) = 0d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:¬j = ih2:i = j⊢ (starRingEnd ℂ) 0 = (ω d ^ i.val) ^ (-1).vald:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:¬j = ih2:¬i = j⊢ (starRingEnd ℂ) 0 = 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ (starRingEnd ℂ) (ω d ^ j.val) = (ω d ^ i.val) ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ (starRingEnd ℂ) (ω d ^ i.val) = (ω d ^ i.val) ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ (starRingEnd ℂ) (ω d) ^ i.val = (ω d ^ i.val) ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ (starRingEnd ℂ) (ω d) ^ i.val = (ω d ^ (-1).val) ^ i.val have homega : (starRingEnd ℂ ) (ω d) = ω d ^ (-1 : ℤ) := d:ℕinst✝:NeZero d⊢ (Z d).conjTranspose = Z d ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ (starRingEnd ℂ) (Complex.exp (2 * ↑Real.pi * Complex.I / ↑d)) = Complex.exp (2 * ↑Real.pi * Complex.I / ↑d) ^ (-1) d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ Complex.exp ((starRingEnd ℂ) (2 * ↑Real.pi * Complex.I / ↑d)) = Complex.exp (↑(-1) * (2 * ↑Real.pi * Complex.I / ↑d)) d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ Complex.exp (star (2 * ↑Real.pi * Complex.I / ↑d)) = Complex.exp (↑(-1) * (2 * ↑Real.pi * Complex.I / ↑d)) d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = j⊢ Complex.exp (-(2 * ↑Real.pi * Complex.I) / ↑d) = Complex.exp (-(2 * ↑Real.pi * Complex.I / ↑d)) All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = jhomega:(starRingEnd ℂ) (ω d) = ω d ^ (-1)⊢ (ω d ^ (↑(-1)).val) ^ i.val = (ω d ^ (-1).val) ^ i.val d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:i = jhomega:(starRingEnd ℂ) (ω d) = ω d ^ (-1)⊢ ↑(-1) = -1 All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:¬i = j⊢ (starRingEnd ℂ) (ω d ^ j.val) = 0 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:j = ih2:¬i = j⊢ False All goals completed! 🐙 d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:¬j = ih2:i = j⊢ (starRingEnd ℂ) 0 = (ω d ^ i.val) ^ (-1).val d:ℕinst✝:NeZero di:ZMod dj:ZMod dhdiag:Z d = Matrix.diagonal fun i => ω d ^ i.valh1:¬j = ih2:i = j⊢ False All goals completed! 🐙 All goals completed! 🐙
Lean codelemma Z_pow_eq_mod_d : (x: ℕ) → (y: ℕ) → (x % d = y % d → Z d ^ x = Z d ^ y ) := d:ℕinst✝:NeZero d⊢ ∀ (x y : ℕ), x % d = y % d → Z d ^ x = Z d ^ y -- This is exactly the same proof as for X, -- maybe we can consolidate intro x d:ℕinst✝:NeZero dx:ℕy:ℕ⊢ x % d = y % d → Z d ^ x = Z d ^ y d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ x = Z d ^ y d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ (d * (x / d) + x % d) = Z d ^ y d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ (d * (x / d) + x % d) = Z d ^ (d * (y / d) + y % d) d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ (Z d ^ d) ^ (x / d) * Z d ^ (x % d) = (Z d ^ d) ^ (y / d) * Z d ^ (y % d) d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ 1 ^ (x / d) * Z d ^ (x % d) = 1 ^ (y / d) * Z d ^ (y % d) d:ℕinst✝:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ (x % d) = Z d ^ (y % d) All goals completed! 🐙
Lean codelemma Z_inv_pow : (x: ZMod d) → ((Z d)^(x.val)).conjTranspose = (Z d)^((-x).val):= d:ℕinst✝:NeZero d⊢ ∀ (x : ZMod d), (Z d ^ x.val).conjTranspose = Z d ^ (-x).val -- This is exactly the same proof as for X, -- maybe we can consolidate d:ℕinst✝:NeZero dx:ZMod d⊢ (Z d ^ x.val).conjTranspose = Z d ^ (-x).val d:ℕinst✝:NeZero dx:ZMod d⊢ Z d ^ ((-1).val * x.val) = Z d ^ (-x).val d:ℕinst✝:NeZero dx:ZMod d⊢ (-1).val * x.val % d = (-x).val % d d:ℕinst✝:NeZero dx:ZMod d⊢ (-x).val = (-x).val % d All goals completed! 🐙