Search ยท Algorithms

Amplitude amplification

Theorem statement

Suppose $A$ is an $n$-qubit unitary such that $A\ket{0}=\sin(\theta)\ket{\psi_1}+\cos(\theta)\ket{\psi_0}$, where $\langle\psi_1|\psi_0\rangle=0$. Let $Q=A(2\ket{0}\!\bra{0}-I)A^\dagger(2\ket{\psi_0}\!\bra{\psi_0}-I)$. Then for every $k\geq 0$, $$ Q^kA\ket{0} = \sin((2k+1)\theta)\ket{\psi_1}+\cos((2k+1)\theta)\ket{\psi_0}. $$

Copy a short prompt with the import, theorem name, citations, and public source link.

Open Lean source