The SWAP test

The SWAP test estimates the overlap |<psi|phi>|^2 of two n-qubit states: run the Hadamard test with the unitary that swaps the two registers [BCWdW01, main.tex:291]. Measuring the control yields outcome 1 with probability (1 - |<psi|phi>|^2)/2 [BCWdW01, main.tex:328].

def QuantumAlg.swapRegistersPerm (n : ℕ) : Equiv.Perm (Fin (2 ^ (n + n)))

The permutation of joint basis labels that exchanges two n-qubit registers.

Equations

• QuantumAlg.swapRegistersPerm n = (QuantumAlg.prodEquiv.symm.trans (Equiv.prodComm (Fin (2 ^ n)) (Fin (2 ^ n)))).trans QuantumAlg.prodEquiv

def QuantumAlg.swapRegisters (n : ℕ) : Gate (n + n)

The register-swap gate SWAP : Gate (n + n).

Equations

• QuantumAlg.swapRegisters n = QuantumAlg.Gate.ofPerm (QuantumAlg.swapRegistersPerm n)

theorem QuantumAlg.swapRegisters_mem_unitaryGroup (n : ℕ) : (swapRegisters n).op ∈ Matrix.unitaryGroup (Fin (2 ^ (n + n))) ℂ

theorem QuantumAlg.swapRegisters_apply_tensor {n : ℕ} (psi phi : PureState n) : (swapRegisters n).apply (psi.tensor phi) = phi.tensor psi

The register swap exchanges tensor factors.

noncomputable def QuantumAlg.swapTest (n : ℕ) : Gate (1 + (n + n))

The SWAP test circuit: the Hadamard test of the register swap.

Equations

• QuantumAlg.swapTest n = QuantumAlg.hadamardTest (QuantumAlg.swapRegisters n)

theorem QuantumAlg.re_inner_swapRegisters {n : ℕ} (psi phi : PureState n) : (inner ℂ (psi.tensor phi) ((swapRegisters n).apply (psi.tensor phi))).re = ‖inner ℂ psi phi‖ ^ 2

Re <psi ⊗ phi, SWAP (psi ⊗ phi)> = |<psi|phi>|^2.

theorem QuantumAlg.swapTest_probQubit0_zero {n : ℕ} (psi phi : PureState n) : ((swapTest n).apply (PureState.ket0.tensor (psi.tensor phi))).probQubit0 0 = (1 + ‖inner ℂ psi phi‖ ^ 2) / 2

SWAP test, outcome 0 [BCWdW01, main.tex:328].

theorem QuantumAlg.SwapTest.main {n : ℕ} (psi phi : PureState n) : ((swapTest n).apply (PureState.ket0.tensor (psi.tensor phi))).probQubit0 1 = (1 - ‖inner ℂ psi phi‖ ^ 2) / 2

SWAP test, outcome 1 [BCWdW01, main.tex:328].