Estimation ยท Primitives
Hadamard test
Theorem statement
Let $U$ be a unitary. Then for any state $\ket{\psi}$, the output state $\ket{\psi'} = \mathtt{H}_1(\ket{0}\!\bra{0}\otimes I+\ket{1}\!\bra{1}\otimes U)\mathtt{H}_1\ket{0,\psi}$ satisfies
$$
\bra{\psi'}(\ket{0}\!\bra{0}\otimes I)\ket{\psi'}
=
(1+\mathfrak{Re}\{\bra{\psi}U\ket{\psi}\})/2.
$$
- $\mathtt{H}_1$
- Hadamard gate acting on the control qubit.
Sources
- A Polynomial Quantum Algorithm for Approximating the Jones Polynomial
Dorit Aharonov, Vaughan Jones, Zeph Landau, 2006
- Quantum fingerprinting
Harry Buhrman, Richard Cleve, John Watrous, Ronald de Wolf, 2001
- Quantum Computation and Quantum Information
Michael A. Nielsen, Isaac L. Chuang, 2010
Lean context
- Lean declaration
QuantumAlg.HadamardTest.main
Copy a short prompt with the import, theorem name, citations, and public source link.