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

theorem Matrix.conjTranspose_fin_one {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] (a : α) : !![a].conjTranspose = !![star a]

theorem Matrix.conjTranspose_fin_two {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] (a b c d : α) : !![a, b; c, d].conjTranspose = !![star a, star c; star b, star d]

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_2⟩

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

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

Equations

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