Phase estimation ยท Primitives
Phase kickback (generalized)
Theorem statement
Let $U$ be a unitary with eigenstate $\ket{\psi}$ such that $U\ket{\psi}=e^{i\phi}\ket{\psi}$. Let $\mathtt{CU}$ denote the controlled version of $U$. Then for any coefficients $a,b\in\mathbb{C}$,
$$
\mathtt{CU}\bigl((a\ket{0}+b\ket{1})\ket{\psi}\bigr)
=
(a\ket{0}+e^{i\phi}b\ket{1})\ket{\psi}.
$$
- $\mathtt{CU}$
- Controlled version of the unitary U.
Sources
- Quantum Algorithms Revisited
Richard Cleve, Artur Ekert, Chiara Macchiavello, Michele Mosca, 1998
Lean context
- Lean declaration
QuantumAlg.GeneralizedPhaseKickback.main
Copy a short prompt with the import, theorem name, citations, and public source link.