Documentation

LeanPool.LeanQuantumAlg.Primitives.HadamardTest

The Hadamard test #

The Hadamard test estimates Re <psi| U |psi> for a unitary U: prepare |0> ⊗ psi, apply H on the control, the controlled U, and H again, then measure the control qubit. The outcome probabilities are

P(0) = (1 + Re <psi| U |psi>)/2, P(1) = (1 - Re <psi| U |psi>)/2.

Pure-state normalization and gate unitarity are carried by the PureState and Gate types themselves.

source
noncomputable def QuantumAlg.hadamardTest {n : ℕ} (U : Gate n) :
Gate (1 + n)

The Hadamard test circuit (H ⊗ I) · c-U · (H ⊗ I).

Equations
Instances For
    source
    theorem QuantumAlg.hadamardTest_mem_unitaryGroup {n : ℕ} (U : Gate n) :
    (hadamardTest U).op ∈ Matrix.unitaryGroup (Fin (2 ^ (1 + n))) ℂ

    The Hadamard test is unitary.

    source
    theorem QuantumAlg.hadamardTest_applyVec_ket0_tensor {n : ℕ} (U : Gate n) (psi : PureState n) :
    (hadamardTest U).op.applyVec (PureState.ket0.vec.tensor psi.vec) = 2⁻¹ • (PureState.ket0.vec.tensor (psi.vec + (U.apply psi).vec) + PureState.ket1.vec.tensor (psi.vec - (U.apply psi).vec))

    Raw-vector pre-measurement state of the Hadamard test.

    source
    theorem QuantumAlg.hadamardTest_apply_ket0_tensor {n : ℕ} (U : Gate n) (psi : PureState n) :
    ((hadamardTest U).apply (PureState.ket0.tensor psi)).vec = 2⁻¹ • (PureState.ket0.vec.tensor (psi.vec + (U.apply psi).vec) + PureState.ket1.vec.tensor (psi.vec - (U.apply psi).vec))

    The pre-measurement state of the Hadamard test.

    source
    theorem QuantumAlg.HadamardTest.main {n : ℕ} {U : Gate n} (psi : PureState n) :
    ((hadamardTest U).apply (PureState.ket0.tensor psi)).probQubit0 0 = (1 + (inner ℂ psi (U.apply psi)).re) / 2

    Hadamard test, outcome 0.

    source
    theorem QuantumAlg.hadamardTest_probQubit0_one {n : ℕ} {U : Gate n} (psi : PureState n) :
    ((hadamardTest U).apply (PureState.ket0.tensor psi)).probQubit0 1 = (1 - (inner ℂ psi (U.apply psi)).re) / 2

    Hadamard test, outcome 1.