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

@[simp]

theorem Matrix.neg_unitary_val {α : Type u_2} [DecidableEq α] [Fintype α] (u : ↥𝐔[α]) : ↑(-u) = -↑u

@[simp]

theorem Matrix.star_kron {α : Type u_2} {β : Type u_3} (a : Matrix α α ℂ) (b : Matrix β β ℂ) : star (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) a b) = kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (star a) (star b)

theorem Matrix.kron_unitary {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) : kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑a ↑b ∈ 𝐔[α × β]

def Matrix.unitary_kron {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) : ↥𝐔[α × β]

Equations

• Matrix.unitary_kron a b = ⟨Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑a ↑b, ⋯⟩

def Matrix.«term_⊗ᵤ_» : Lean.TrailingParserDescr

Equations

• Matrix.«term_⊗ᵤ_» = Lean.ParserDescr.trailingNode `Matrix.«term_⊗ᵤ_» 1022 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ᵤ ") (Lean.ParserDescr.cat `term 60))

@[simp]

theorem Matrix.unitary_kron_apply {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : ↥𝐔[α]) (b : ↥𝐔[β]) (i₁ i₂ : α) (j₁ j₂ : β) : ↑(unitary_kron a b) (i₁, j₁) (i₂, j₂) = ↑a i₁ i₂ * ↑b j₁ j₂

@[simp]

theorem Matrix.unitary_kron_one_one {α : Type u_2} {β : Type u_3} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] : unitary_kron 1 1 = 1

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.

@[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⁻¹