Query algorithms ยท Primitives
Phase kickback
Theorem statement
Let $O_f$ be a unitary such that $O_f\ket{x,y}=\ket{x,y\oplus f(x)}$ for some Boolean function $f:\{0,1\}^n\to\{0,1\}$. Then for $\ket{-}=(\ket{0}-\ket{1})/\sqrt{2}$,
$$
O_f(\ket{x}\ket{-})
=
(-1)^{f(x)}\ket{x}\ket{-}.
$$
Sources
- Quantum Computing: Lecture Notes
Ronald de Wolf, 2019
Lean context
- Lean declaration
QuantumAlg.PhaseKickback.main
Copy a short prompt with the import, theorem name, citations, and public source link.