Named gates #

The standard named gates as Components (concrete instances built on the Core gate framework LeanPool.LeanQuantumAlg.Gate). Raw matrices are first stated as HilbertOperators, then bundled into Gates with their unitarity proofs.

Pauli, Hadamard, and CNOT #

source

noncomputable def QuantumAlg.Gate.HOp :

HilbertOperator 1

Raw Hadamard operator H = (1/sqrt 2) [[1, 1], [1, -1]].

Equations

QuantumAlg.Gate.HOp = QuantumAlg.PureState.invSqrt2 • !![1, 1; 1, -1]

Instances For

source

theorem QuantumAlg.Gate.HOp_mem_unitaryGroup :

HOp ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

noncomputable def QuantumAlg.Gate.H :

Gate 1

The Hadamard gate.

Equations

QuantumAlg.Gate.H = QuantumAlg.Gate.ofUnitary QuantumAlg.Gate.HOp QuantumAlg.Gate.HOp_mem_unitaryGroup

Instances For

source

def QuantumAlg.Gate.X :

Gate 1

The Pauli-X (NOT) gate, as the basis permutation |0> ↔ |1>.

Equations

QuantumAlg.Gate.X = QuantumAlg.Gate.ofPerm (Equiv.swap 0 1)

Instances For

source

def QuantumAlg.Gate.YOp :

HilbertOperator 1

Raw Pauli-Y operator [[0, -i], [i, 0]].

Equations

QuantumAlg.Gate.YOp = !![0, -Complex.I; Complex.I, 0]

Instances For

source

theorem QuantumAlg.Gate.YOp_mem_unitaryGroup :

YOp ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

def QuantumAlg.Gate.Y :

Gate 1

The Pauli-Y gate.

Equations

QuantumAlg.Gate.Y = QuantumAlg.Gate.ofUnitary QuantumAlg.Gate.YOp QuantumAlg.Gate.YOp_mem_unitaryGroup

Instances For

source

def QuantumAlg.Gate.ZOp :

HilbertOperator 1

Raw Pauli-Z operator [[1, 0], [0, -1]].

Equations

QuantumAlg.Gate.ZOp = !![1, 0; 0, -1]

Instances For

source

theorem QuantumAlg.Gate.ZOp_mem_unitaryGroup :

ZOp ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

def QuantumAlg.Gate.Z :

Gate 1

The Pauli-Z gate.

Equations

QuantumAlg.Gate.Z = QuantumAlg.Gate.ofUnitary QuantumAlg.Gate.ZOp QuantumAlg.Gate.ZOp_mem_unitaryGroup

Instances For

source

def QuantumAlg.Gate.CNOT :

Gate 2

The controlled-NOT gate on two qubits, control = qubit 0.

Equations

QuantumAlg.Gate.CNOT = QuantumAlg.Gate.ofPerm (Equiv.swap 2 3)

Instances For

source

theorem QuantumAlg.Gate.X_mem_unitaryGroup :

X.op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

theorem QuantumAlg.Gate.CNOT_mem_unitaryGroup :

CNOT.op ∈ Matrix.unitaryGroup (Fin (2 ^ 2)) ℂ

source

theorem QuantumAlg.Gate.Y_mem_unitaryGroup :

Y.op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

theorem QuantumAlg.Gate.Z_mem_unitaryGroup :

Z.op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

theorem QuantumAlg.Gate.H_mem_unitaryGroup :

H.op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

@[simp]

theorem QuantumAlg.Gate.H_apply_ket0 :

H.apply PureState.ket0 = PureState.ketPlus

H |0> = |+>.

source

@[simp]

theorem QuantumAlg.Gate.H_apply_ket1 :

H.apply PureState.ket1 = PureState.ketMinus

H |1> = |->.

source

@[simp]

theorem QuantumAlg.Gate.H_applyVec_ket0 :

H.applyVec PureState.ket0.vec = PureState.ketPlus.vec

source

@[simp]

theorem QuantumAlg.Gate.H_applyVec_ket1 :

H.applyVec PureState.ket1.vec = PureState.ketMinus.vec

source

theorem QuantumAlg.Gate.CNOT_apply_ket (x : Fin (2 ^ 2)) :

CNOT.apply (PureState.ket x) = PureState.ket ((Equiv.swap 2 3) x)

CNOT permutes the basis by swapping |10> ↔ |11> (indices 2 ↔ 3).

source

@[simp]

theorem QuantumAlg.Gate.X_apply_ket0 :

X.apply PureState.ket0 = PureState.ket1

X |0> = |1>.

source

@[simp]

theorem QuantumAlg.Gate.X_apply_ket1 :

X.apply PureState.ket1 = PureState.ket0

X |1> = |0>.

source

@[simp]

theorem QuantumAlg.Gate.X_applyVec_ket0 :

X.applyVec PureState.ket0.vec = PureState.ket1.vec

source

@[simp]

theorem QuantumAlg.Gate.X_applyVec_ket1 :

X.applyVec PureState.ket1.vec = PureState.ket0.vec

source

@[simp]

theorem QuantumAlg.Gate.Z_apply_ket0 :

Z.apply PureState.ket0 = PureState.ket0

Z |0> = |0>.

source

@[simp]

theorem QuantumAlg.Gate.Z_applyVec_ket0 :

Z.applyVec PureState.ket0.vec = PureState.ket0.vec

source

@[simp]

theorem QuantumAlg.Gate.Z_applyVec_ket1 :

Z.applyVec PureState.ket1.vec = -PureState.ket1.vec

Raw-vector form of Z |1> = -|1>.

source

theorem QuantumAlg.Gate.H_mul_H :

H * H = 1

H * H = 1: the Hadamard gate is an involution.

source

@[simp]

theorem QuantumAlg.Gate.H_apply_ketPlus :

H.apply PureState.ketPlus = PureState.ket0

H |+> = |0>.

source

@[simp]

theorem QuantumAlg.Gate.H_apply_ketMinus :

H.apply PureState.ketMinus = PureState.ket1

H |-> = |1>.

`CNOT` on the tensor basis #

source

@[simp]

theorem QuantumAlg.Gate.CNOT_apply_ket0_tensor_ket0 :

CNOT.apply (PureState.ket0.tensor PureState.ket0) = PureState.ket0.tensor PureState.ket0

CNOT |00> = |00>.

source

@[simp]

theorem QuantumAlg.Gate.CNOT_apply_ket0_tensor_ket1 :

CNOT.apply (PureState.ket0.tensor PureState.ket1) = PureState.ket0.tensor PureState.ket1

CNOT |01> = |01>.

source

@[simp]

theorem QuantumAlg.Gate.CNOT_apply_ket1_tensor_ket0 :

CNOT.apply (PureState.ket1.tensor PureState.ket0) = PureState.ket1.tensor PureState.ket1

CNOT |10> = |11>.

source

@[simp]

theorem QuantumAlg.Gate.CNOT_apply_ket1_tensor_ket1 :

CNOT.apply (PureState.ket1.tensor PureState.ket1) = PureState.ket1.tensor PureState.ket0

CNOT |11> = |10>.

source

@[simp]

theorem QuantumAlg.Gate.CNOT_applyVec_ket0_tensor_ket0 :

CNOT.applyVec (PureState.ket0.vec.tensor PureState.ket0.vec) = PureState.ket0.vec.tensor PureState.ket0.vec

source

@[simp]

theorem QuantumAlg.Gate.CNOT_applyVec_ket0_tensor_ket1 :

CNOT.applyVec (PureState.ket0.vec.tensor PureState.ket1.vec) = PureState.ket0.vec.tensor PureState.ket1.vec

source

@[simp]

theorem QuantumAlg.Gate.CNOT_applyVec_ket1_tensor_ket0 :

CNOT.applyVec (PureState.ket1.vec.tensor PureState.ket0.vec) = PureState.ket1.vec.tensor PureState.ket1.vec

source

@[simp]

theorem QuantumAlg.Gate.CNOT_applyVec_ket1_tensor_ket1 :

CNOT.applyVec (PureState.ket1.vec.tensor PureState.ket1.vec) = PureState.ket1.vec.tensor PureState.ket0.vec

Rotation gates (QSP / QNN conventions) #

source

noncomputable def QuantumAlg.rotZOp (phi : ℝ) :

HilbertOperator 1

Raw processing rotation e^{i phi Z}.

Equations

QuantumAlg.rotZOp phi = !![Complex.exp (↑phi * Complex.I), 0; 0, Complex.exp (-(↑phi * Complex.I))]

Instances For

source

theorem QuantumAlg.rotZOp_mem_unitaryGroup (phi : ℝ) :

rotZOp phi ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

noncomputable def QuantumAlg.rotZ (phi : ℝ) :

Gate 1

The processing rotation e^{i phi Z}.

Equations

QuantumAlg.rotZ phi = QuantumAlg.Gate.ofUnitary (QuantumAlg.rotZOp phi) ⋯

Instances For

source

theorem QuantumAlg.rotZ_mul_rotZ (a b : ℝ) :

rotZ a * rotZ b = rotZ (a + b)

source

@[simp]

theorem QuantumAlg.rotZ_zero :

rotZ 0 = 1

source

theorem QuantumAlg.rotZ_mem_unitaryGroup (phi : ℝ) :

(rotZ phi).op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

theorem QuantumAlg.rotZ_comm (a b : ℝ) :

rotZ a * rotZ b = rotZ b * rotZ a

source

theorem QuantumAlg.rotZ_neg_mul_rotZ (phi : ℝ) :

rotZ (-phi) * rotZ phi = 1

source

theorem QuantumAlg.rotZ_mul_rotZ_neg (phi : ℝ) :

rotZ phi * rotZ (-phi) = 1

source

noncomputable def QuantumAlg.rotYOp (theta : ℝ) :

HilbertOperator 1

Raw standard R_Y(theta).

Equations

QuantumAlg.rotYOp theta = !![↑(Real.cos (theta / 2)), -↑(Real.sin (theta / 2)); ↑(Real.sin (theta / 2)), ↑(Real.cos (theta / 2))]

Instances For

source

theorem QuantumAlg.rotYOp_mem_unitaryGroup (theta : ℝ) :

rotYOp theta ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

noncomputable def QuantumAlg.rotY (theta : ℝ) :

Gate 1

The standard R_Y(theta) gate.

Equations

QuantumAlg.rotY theta = QuantumAlg.Gate.ofUnitary (QuantumAlg.rotYOp theta) ⋯

Instances For

source

noncomputable def QuantumAlg.rotZStd (phi : ℝ) :

Gate 1

The standard R_Z(phi) = e^{-i phi Z/2}.

Equations

QuantumAlg.rotZStd phi = QuantumAlg.rotZ (-(phi / 2))

Instances For

source

@[simp]

theorem QuantumAlg.rotZStd_zero :

rotZStd 0 = 1

source

theorem QuantumAlg.rotY_mem_unitaryGroup (theta : ℝ) :

(rotY theta).op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

source

theorem QuantumAlg.rotZStd_mem_unitaryGroup (phi : ℝ) :

(rotZStd phi).op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

Documentation

LeanPool.LeanQuantumAlg.Core.Components.Gates

Named gates #

Pauli, Hadamard, and CNOT #

`CNOT` on the tensor basis #

Rotation gates (QSP / QNN conventions) #

Named gates #

Pauli, Hadamard, and CNOT #

CNOT on the tensor basis #

Rotation gates (QSP / QNN conventions) #

`CNOT` on the tensor basis #