Quantum theory and operations specific to qubits.

• Standard named (single-qubit) gates: Z, X, Y, H, S, T
• Controlled versions of gates
• Completeness of the PPT test: a state is separable iff it is PPT.
• Fidelity for qubits: F(ρ,σ) = 2√(ρ.det * σ.det).
• The singlet/triplet split.

@[reducible, inline]

abbrev Qubit : Type

Equations

• Qubit = Fin 2

def matrix_expand : Lean.ParserDescr

Proves goals equating small matrices by expanding out products and simpliying standard Real arithmetic.

Equations

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

def Qubit.Z : ↥𝐔[Qubit]

The Pauli Z gate on a qubit.

Equations

• Qubit.Z = ⟨!![1, 0; 0, -1], Qubit.Z._proof_1⟩

def Qubit.X : ↥𝐔[Qubit]

The Pauli X gate on a qubit.

Equations

• Qubit.X = ⟨!![0, 1; 1, 0], Qubit.X._proof_1⟩

def Qubit.Y : ↥𝐔[Qubit]

The Pauli Y gate on a qubit.

Equations

• Qubit.Y = ⟨!![0, -Complex.I; Complex.I, 0], Qubit.Y._proof_1⟩

noncomputable def Qubit.H : ↥𝐔[Qubit]

The H gate, a Hadamard gate, on a qubit.

Equations

• Qubit.H = ⟨√(1 / 2) • !![1, 1; 1, -1], Qubit.H._proof_2⟩

def Qubit.S : ↥𝐔[Qubit]

The S gate, or Rz(π/2) rotation on a qubit.

Equations

• Qubit.S = ⟨!![1, 0; 0, Complex.I], Qubit.S._proof_1⟩

noncomputable def Qubit.T : ↥𝐔[Qubit]

The T gate, or Rz(π/4) rotation on a qubit.

Equations

• Qubit.T = ⟨!![1, 0; 0, (1 + Complex.I) / ↑√2], Qubit.T._proof_1⟩

@[simp]

theorem Qubit.Z_sq : Z * Z = 1

@[simp]

theorem Qubit.X_sq : X * X = 1

@[simp]

theorem Qubit.Y_sq : Y * Y = 1

@[simp]

theorem Qubit.H_sq : H * H = 1

@[simp]

theorem Qubit.S_sq : S * S = Z

@[simp]

theorem Qubit.T_sq : T * T = S

@[simp]

theorem Qubit.X_Y_anticomm : X * Y = -Y * X

The anticommutator {X,Y} is zero. Marked simp as to put Pauli products in a canonical Y-X-Z order.

theorem Qubit.Y_Z_anticomm : Z * Y = -Y * Z

The anticommutator {Y,Z} is zero.

theorem Qubit.Z_X_anticomm : Z * X = -X * Z

The anticommutator {Z,X} is zero.

@[simp]

theorem Qubit.H_mul_X_eq_Z_mul_H : H * X = Z * H

@[simp]

theorem Qubit.H_mul_Z_eq_X_mul_H : H * Z = X * H

@[simp]

theorem Qubit.S_Z_comm : Z * S = S * Z

@[simp]

theorem Qubit.T_Z_comm : Z * T = T * Z

@[simp]

theorem Qubit.S_T_comm : S * T = T * S

def Qubit.controllize {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) : ↥𝐔[Qubit × k]

Given a unitary U on some Hilbert space k, we have the controllized version that acts on Fin 2 ⊗ k where U is conditionally applied if the first qubit is 1.

Equations

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

def Qubit.«termC[_]» : Lean.ParserDescr

Equations

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

def Qubit.CNOT : ↥𝐔[Fin 2 × Fin 2]

Controlled-NOT gate on two qubits. The first qubit is the control and the second qubit is the target.

Equations

• Qubit.CNOT = Qubit.controllize Qubit.X

theorem Qubit.CNOT_matrix : (Matrix.reindex finProdFinEquiv finProdFinEquiv) ↑CNOT = ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, 0, 1], ![0, 0, 1, 0]]

The matrix representation of CNOT is the standard 4×4 permutation matrix.

@[simp]

theorem Qubit.controllize_apply_zero_zero {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) (j₁ j₂ : k) : ↑(controllize g) (0, j₁) (0, j₂) = ↑1 j₁ j₂

@[simp]

theorem Qubit.controllize_apply_zero_one {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) (j₁ j₂ : k) : ↑(controllize g) (0, j₁) (1, j₂) = 0

@[simp]

theorem Qubit.controllize_apply_one_zero {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) (j₁ j₂ : k) : ↑(controllize g) (1, j₁) (0, j₂) = 0

@[simp]

theorem Qubit.controllize_apply_one_one {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) (j₁ j₂ : k) : ↑(controllize g) (1, j₁) (1, j₂) = ↑g j₁ j₂

@[simp]

theorem Qubit.controllize_mul {k : Type u_1} [Fintype k] [DecidableEq k] (g₁ g₂ : ↥𝐔[k]) : controllize g₁ * controllize g₂ = controllize (g₁ * g₂)

@[simp]

theorem Qubit.controllize_one {k : Type u_1} [Fintype k] [DecidableEq k] : controllize 1 = 1

@[simp]

theorem Qubit.controllize_mul_inv {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) : controllize g * controllize g⁻¹ = 1

@[simp]

theorem Qubit.X_controllize_X {k : Type u_1} [Fintype k] [DecidableEq k] (g : ↥𝐔[k]) : Matrix.unitary_kron X 1 * controllize g * Matrix.unitary_kron X 1 = Matrix.unitary_kron 1 g * controllize g⁻¹