Quantum circuits

The state of an n-qubit register is a vector of ℂ^{{0,1}^n} (Cslib.Quantum.Qubits), with computational basis |x⟩ (Cslib.Quantum.ket) for bit strings x : Fin n → Bool. A gate is a unitary matrix on k qubits (Cslib.Quantum.Gate). Applied to an ordered list A of k distinct qubits of the register, written U[A] in Shi, it acts on those qubits and leaves the others alone (Cslib.Quantum.PlacedGate): ⟨y| U[A] |x⟩ = U(y ∘ A, x ∘ A) when y and x agree off A, and 0 otherwise (Cslib.Quantum.PlacedGate.matrix_apply). A circuit is a sequence of placed gates (Cslib.Quantum.Circuit); its unitary is the product U_m ⋯ U_1 of its gates, the first gate acting first (Cslib.Quantum.Circuit.matrix), and it acts on states as a linear isometric equivalence (Cslib.Quantum.Circuit.eval).

At the end of a computation the whole register is measured in the computational basis: a unit state ψ gives outcome y with probability |ψ_y|² (Cslib.Quantum.measure and Cslib.Quantum.measureProb, from Complexity/Foundations/Quantum/Measurement.lean). This is the model of Arora, Barak, Chapter 10: pure states, gates on a bounded number of qubits, and a single final measurement in the computational basis. Mixed states and intermediate measurements are not modelled; Arora and Barak note that they add no power. A gate set is a set of gates of any arities (Cslib.Quantum.Circuit.IsOver). This file provides the Hadamard gate and the classical reversible gates (Cslib.Quantum.Gate.hadamard, Cslib.Quantum.Gate.ofPerm, Cslib.Quantum.Gate.not, Cslib.Quantum.Gate.cnot, Cslib.Quantum.Gate.toffoli); no particular gate set is fixed here.

As in the quantum query model (Complexity/Computability/QueryComplexity/Quantum/Search.lean), states are vectors of a Euclidean space over ℂ. Gates and circuit unitaries are elements of Mathlib's Matrix.unitaryGroup, acting on states through Matrix.toEuclideanCLM and Unitary.linearIsometryEquiv (Cslib.Quantum.unitaryEquiv). Placing a k-qubit unitary on the qubits A is a monoid homomorphism (Cslib.Quantum.place).

Main definitions

• Cslib.Quantum.Qubits: the n-qubit state space.
• Cslib.Quantum.unitaryEquiv: a unitary matrix as a linear isometric equivalence.
• Cslib.Quantum.Gate, Cslib.Quantum.PlacedGate: gates, and gates applied to chosen qubits.
• Cslib.Quantum.splitEquiv, Cslib.Quantum.place: splitting the register along chosen qubits, and placing a unitary on them.
• Cslib.Quantum.Circuit, Cslib.Quantum.Circuit.matrix, Cslib.Quantum.Circuit.eval: circuits, their unitaries and their action on states.
• Cslib.Quantum.Circuit.run, Cslib.Quantum.Circuit.measure: the final state of a circuit started in a basis state, and the distribution of its measurement.
• Cslib.Quantum.Circuit.IsOver: a circuit whose gates lie in a gate set.
• Cslib.Quantum.Gate.hadamard, Cslib.Quantum.Gate.ofPerm: the Hadamard gate and the classical reversible gates, among them Cslib.Quantum.Gate.not, Cslib.Quantum.Gate.cnot and Cslib.Quantum.Gate.toffoli.

Main results

• Cslib.Quantum.place_apply, Cslib.Quantum.PlacedGate.matrix_apply: the entries of a placed unitary.
• Cslib.Quantum.PlacedGate.eval_ket_apply: a placed gate maps |x⟩ to its column x.
• Cslib.Quantum.Circuit.matrix_append, Cslib.Quantum.Circuit.eval_append: running two circuits in sequence.
• Cslib.Quantum.Circuit.norm_eval: circuits preserve norms.
• Cslib.Quantum.PlacedGate.eval_ofPerm_ket: a classical reversible gate permutes basis states.
• Cslib.Quantum.Gate.hadamard_mul_self: the Hadamard gate is its own inverse.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• Y. Shi, Both Toffoli and Controlled-NOT need little help to do universal quantum computation, §2 (arXiv:quant-ph/0205115v2)

States and measurement

@[reducible, inline]

abbrev Cslib.Quantum.Qubits (n : ℕ) : Type

The state space ℂ^{{0,1}^n} of an n-qubit register, whose computational basis is indexed by bit strings Fin n → Bool.

noncomputable def Cslib.Quantum.unitaryEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) : EuclideanSpace ℂ ι ≃ₗᵢ[ℂ] EuclideanSpace ℂ ι

A unitary matrix, as a linear isometric equivalence of Euclidean space.

@[simp]

theorem Cslib.Quantum.unitaryEquiv_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (ψ : EuclideanSpace ℂ ι) : ((unitaryEquiv U) ψ).ofLp = (↑U).mulVec ψ.ofLp

theorem Cslib.Quantum.unitaryEquiv_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U V : ↥(Matrix.unitaryGroup ι ℂ)) (ψ : EuclideanSpace ℂ ι) : (unitaryEquiv (U * V)) ψ = (unitaryEquiv U) ((unitaryEquiv V) ψ)

@[simp]

theorem Cslib.Quantum.unitaryEquiv_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : EuclideanSpace ℂ ι) : (unitaryEquiv 1) ψ = ψ

Gates

@[reducible, inline]

abbrev Cslib.Quantum.Gate (k : ℕ) : Submonoid (Matrix (Fin k → Bool) (Fin k → Bool) ℂ)

A quantum gate on k qubits: a unitary matrix indexed by {0,1}^k.

structure Cslib.Quantum.PlacedGate (n : ℕ) : Type

A gate U[A] applied to an ordered list A of distinct qubits of an n-qubit register Shi.

• arity : ℕ

  The number of qubits the gate acts on.

• gate : ↥(Gate self.arity)

  The gate.

• wires : Fin self.arity ↪ Fin n

  The qubits it acts on, in order.

noncomputable def Cslib.Quantum.splitEquiv {n k : ℕ} (A : Fin k ↪ Fin n) : (Fin n → Bool) ≃ (Fin k → Bool) × ({ j : Fin n // ¬∃ (i : Fin k), A i = j } → Bool)

Splitting a bit string into its restriction x ∘ A to the qubits A and its values on the other qubits.

@[simp]

theorem Cslib.Quantum.splitEquiv_apply_fst {n k : ℕ} (A : Fin k ↪ Fin n) (x : Fin n → Bool) : ((splitEquiv A) x).1 = x ∘ ⇑A

@[simp]

theorem Cslib.Quantum.splitEquiv_apply_snd {n k : ℕ} (A : Fin k ↪ Fin n) (x : Fin n → Bool) : ((splitEquiv A) x).2 = fun (j : { j : Fin n // ¬∃ (i : Fin k), A i = j }) => x ↑j

@[simp]

theorem Cslib.Quantum.splitEquiv_symm_apply_wire {n k : ℕ} (A : Fin k ↪ Fin n) (b : Fin k → Bool) (r : { j : Fin n // ¬∃ (i : Fin k), A i = j } → Bool) (i : Fin k) : (splitEquiv A).symm (b, r) (A i) = b i

The first component of splitEquiv A determines the values on the qubits A.

theorem Cslib.Quantum.splitEquiv_symm_apply_of_not {n k : ℕ} (A : Fin k ↪ Fin n) (b : Fin k → Bool) (r : { j : Fin n // ¬∃ (i : Fin k), A i = j } → Bool) (j : Fin n) (hj : ¬∃ (i : Fin k), A i = j) : (splitEquiv A).symm (b, r) j = r ⟨j, hj⟩

The second component of splitEquiv A determines the values off the qubits A.

noncomputable def Cslib.Quantum.place {n k : ℕ} (A : Fin k ↪ Fin n) : ↥(Matrix.unitaryGroup (Fin k → Bool) ℂ) →* ↥(Matrix.unitaryGroup (Fin n → Bool) ℂ)

Placing a unitary on the qubits A: the unitary U[A] = U ⊗ I of the whole register, reindexed along splitEquiv A. Placement is multiplicative.

theorem Cslib.Quantum.place_apply {n k : ℕ} (A : Fin k ↪ Fin n) (U : ↥(Matrix.unitaryGroup (Fin k → Bool) ℂ)) (y x : Fin n → Bool) : ↑((place A) U) y x = if ∀ (j : Fin n), (¬∃ (i : Fin k), A i = j) → y j = x j then ↑U (y ∘ ⇑A) (x ∘ ⇑A) else 0

The entries of a placed unitary: ⟨y| U[A] |x⟩ = U(y ∘ A, x ∘ A) when y and x agree off A, and 0 otherwise.

noncomputable def Cslib.Quantum.PlacedGate.matrix {n : ℕ} (g : PlacedGate n) : ↥(Matrix.unitaryGroup (Fin n → Bool) ℂ)

The unitary U[A] of a placed gate on the whole register.

theorem Cslib.Quantum.PlacedGate.matrix_apply {n : ℕ} (g : PlacedGate n) (y x : Fin n → Bool) : ↑g.matrix y x = if ∀ (j : Fin n), (¬∃ (i : Fin g.arity), g.wires i = j) → y j = x j then ↑g.gate (y ∘ ⇑g.wires) (x ∘ ⇑g.wires) else 0

The entries of a placed gate: ⟨y| U[A] |x⟩ = U(y ∘ A, x ∘ A) when y and x agree off A, and 0 otherwise.

noncomputable def Cslib.Quantum.PlacedGate.eval {n : ℕ} (g : PlacedGate n) : Qubits n ≃ₗᵢ[ℂ] Qubits n

The action of a placed gate on states.

theorem Cslib.Quantum.PlacedGate.eval_ket_apply {n : ℕ} (g : PlacedGate n) (x y : Fin n → Bool) : (g.eval (ket x)).ofLp y = ↑g.matrix y x

A placed gate maps the basis state |x⟩ to its column x.

Circuits

@[reducible, inline]

abbrev Cslib.Quantum.Circuit (n : ℕ) : Type

A quantum circuit on n qubits: a sequence of placed gates, applied first to last.

noncomputable def Cslib.Quantum.Circuit.matrix {n : ℕ} : Circuit n → ↥(Matrix.unitaryGroup (Fin n → Bool) ℂ)

The unitary U_m ⋯ U_1 of a circuit with gates U_1, …, U_m.

@[simp]

theorem Cslib.Quantum.Circuit.matrix_nil {n : ℕ} : matrix [] = 1

@[simp]

theorem Cslib.Quantum.Circuit.matrix_cons {n : ℕ} (g : PlacedGate n) (C : Circuit n) : matrix (g :: C) = C.matrix * g.matrix

@[simp]

theorem Cslib.Quantum.Circuit.matrix_append {n : ℕ} (C D : Circuit n) : (C ++ D).matrix = D.matrix * C.matrix

Running C and then D applies D's unitary after C's.

noncomputable def Cslib.Quantum.Circuit.eval {n : ℕ} (C : Circuit n) : Qubits n ≃ₗᵢ[ℂ] Qubits n

The action of a circuit on states.

@[simp]

theorem Cslib.Quantum.Circuit.eval_nil {n : ℕ} (ψ : Qubits n) : (eval []) ψ = ψ

@[simp]

theorem Cslib.Quantum.Circuit.eval_cons {n : ℕ} (g : PlacedGate n) (C : Circuit n) (ψ : Qubits n) : (eval (g :: C)) ψ = C.eval (g.eval ψ)

theorem Cslib.Quantum.Circuit.eval_append {n : ℕ} (C D : Circuit n) (ψ : Qubits n) : (C ++ D).eval ψ = D.eval (C.eval ψ)

theorem Cslib.Quantum.Circuit.norm_eval {n : ℕ} (C : Circuit n) (ψ : Qubits n) : ‖C.eval ψ‖ = ‖ψ‖

Circuits preserve norms.

noncomputable def Cslib.Quantum.Circuit.run {n : ℕ} (C : Circuit n) (x : Fin n → Bool) : Qubits n

The final state of the circuit started in the basis state |x⟩.

@[simp]

theorem Cslib.Quantum.Circuit.norm_run {n : ℕ} (C : Circuit n) (x : Fin n → Bool) : ‖C.run x‖ = 1

noncomputable def Cslib.Quantum.Circuit.measure {n : ℕ} (C : Circuit n) (x : Fin n → Bool) : PMF (Fin n → Bool)

The distribution of the outcome of measuring the final state of C started in |x⟩.

@[simp]

theorem Cslib.Quantum.Circuit.measure_apply {n : ℕ} (C : Circuit n) (x y : Fin n → Bool) : (C.measure x) y = ENNReal.ofReal (‖(C.run x).ofLp y‖ ^ 2)

def Cslib.Quantum.Circuit.IsOver {n : ℕ} (B : Set ((k : ℕ) × ↥(Gate k))) (C : Circuit n) : Prop

The circuit C uses only gates from the gate set B, a set of gates of any arities.

The Hadamard gate and classical reversible gates

noncomputable def Cslib.Quantum.Gate.hadamardMatrix : Matrix Bool Bool ℂ

The Hadamard matrix H = (1/√2) [[1, 1], [1, -1]], indexed by one bit.

theorem Cslib.Quantum.Gate.hadamardMatrix_mem_unitaryGroup : hadamardMatrix ∈ Matrix.unitaryGroup Bool ℂ

theorem Cslib.Quantum.Gate.star_hadamardMatrix : star hadamardMatrix = hadamardMatrix

noncomputable def Cslib.Quantum.Gate.hadamard : ↥(Gate 1)

The Hadamard gate |b⟩ ↦ (|0⟩ + (-1)^b |1⟩)/√2.

theorem Cslib.Quantum.Gate.hadamard_apply (y x : Fin 1 → Bool) : ↑hadamard y x = (if (y 0 && x 0) = true then -1 else 1) * ↑(√2)⁻¹

theorem Cslib.Quantum.Gate.hadamard_mul_self : hadamard * hadamard = 1

The Hadamard gate is its own inverse.

noncomputable def Cslib.Quantum.Gate.ofPerm {k : ℕ} (σ : Equiv.Perm (Fin k → Bool)) : ↥(Gate k)

The classical reversible gate |x⟩ ↦ |σ x⟩ of a permutation σ of {0,1}^k.

theorem Cslib.Quantum.Gate.ofPerm_apply {k : ℕ} (σ : Equiv.Perm (Fin k → Bool)) (y x : Fin k → Bool) : ↑(ofPerm σ) y x = if y = σ x then 1 else 0

noncomputable def Cslib.Quantum.Gate.ofInvolutive {k : ℕ} (f : (Fin k → Bool) → Fin k → Bool) (hf : Function.Involutive f) : ↥(Gate k)

The classical reversible gate of an involution of {0,1}^k.

noncomputable def Cslib.Quantum.Gate.not : ↥(Gate 1)

The NOT gate |b⟩ ↦ |¬b⟩.

noncomputable def Cslib.Quantum.Gate.cnot : ↥(Gate 2)

The controlled NOT gate |a, b⟩ ↦ |a, b ⊕ a⟩.

noncomputable def Cslib.Quantum.Gate.toffoli : ↥(Gate 3)

The Toffoli gate |a, b, c⟩ ↦ |a, b, c ⊕ (a ∧ b)⟩.

theorem Cslib.Quantum.PlacedGate.eval_ofPerm_ket {n k : ℕ} (σ : Equiv.Perm (Fin k → Bool)) (A : Fin k ↪ Fin n) (x : Fin n → Bool) : { arity := k, gate := Gate.ofPerm σ, wires := A }.eval (ket x) = ket ((splitEquiv A).symm (σ (x ∘ ⇑A), ((splitEquiv A) x).2))

A classical reversible gate permutes basis states: σ[A] maps |x⟩ to the basis state that agrees with x off A and equals σ (x ∘ A) on A.