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}.
$$
Sources
- Quantum Computing: Lecture Notes
Ronald de Wolf, 2019
Lean context
- Lean declaration
QuantumAlg.AmplitudeAmplification.main
Copy a short prompt with the import, theorem name, citations, and public source link.